diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 1a3876714548db58912a028c489e70774137913f..95f87fc40b28769344b6d887027f9f0564c36839 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -9,7 +9,7 @@ object DefOps {
     df match {
       case _ : Program => List()
       case u : UnitDef => u.pack 
-      case _ => inPackage(df.owner.get)
+      case _ => df.owner map inPackage getOrElse List()
     }
   }
   
@@ -19,10 +19,10 @@ object DefOps {
     case other => other.owner flatMap inUnit
   }
   
-  def inProgram(df : Definition) : Program = {
+  def inProgram(df : Definition) : Option[Program] = {
     df match {
-      case p : Program => p
-      case other => inProgram(other.owner.get)
+      case p : Program => Some(p)
+      case other => other.owner flatMap inProgram
     }
   }
     
@@ -55,9 +55,13 @@ object DefOps {
   def visibleDefsFrom(df : Definition) : Set[Definition] = {
     var toRet = Map[String,Definition]()
     val asList = 
-      (pathFromRoot(df).reverse flatMap { _.subDefinitions })  ++
-      (unitsInPackage(inProgram(df), inPackage(df)) flatMap { _.subDefinitions } ) ++
-      Seq(inProgram(df)) ++
+      (pathFromRoot(df).reverse flatMap { _.subDefinitions }) ++ {
+        inProgram(df) match {
+          case None => List()
+          case Some(p) => unitsInPackage(p, inPackage(df)) flatMap { _.subDefinitions } 
+        }
+      } ++
+      inProgram(df).toList ++
       ( for ( u <- inUnit(df).toSeq;
               imp <- u.imports;
               impDf <- imp.importedDefs
@@ -125,17 +129,18 @@ object DefOps {
     (pack, finalPath)
   }
 
-  def fullName(df: Definition, fromProgram: Option[Program] = None): String = {
-    val p = fromProgram.getOrElse(inProgram(df))
-
-    val (pr, ds) = pathAsVisibleFrom(p, df)
+  def fullName(df: Definition, fromProgram: Option[Program] = None): String = 
+    fromProgram orElse inProgram(df) match {
+      case None => df.id.name
+      case Some(p) =>
+        val (pr, ds) = pathAsVisibleFrom(p, df)
 
-    (pr ::: ds.flatMap{
-      case _: UnitDef => None
-      case m: ModuleDef if m.isStandalone => None
-      case d => Some(d.id.name)
-    }).mkString(".")
-  }
+        (pr ::: ds.flatMap{
+          case _: UnitDef => None
+          case m: ModuleDef if m.isStandalone => None
+          case d => Some(d.id.name)
+        }).mkString(".")
+    }
 
   def searchByFullName (
     fullName : String,
@@ -152,6 +157,8 @@ object DefOps {
     exploreStandalones : Boolean = true  // Unset this if your path already includes standalone object names
   ) : Option[Definition] = {
   
+    require(inProgram(base).isDefined)
+
     val fullNameList = fullName.split("\\.").toList map scala.reflect.NameTransformer.encode
     require(!fullNameList.isEmpty)
     
@@ -193,8 +200,8 @@ object DefOps {
       path = fullNameList.tail;
       df <- descendDefs(startingPoint,path) 
     ) yield df ) orElse {
-      
-      val program = inProgram(base)
+
+      val program = inProgram(base).get
       val currentPack = inPackage(base)
       val knownPacks = program.units map { _.pack }
       // The correct package has the maximum identifiers
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index bf25c99fc2999e904e6a6adab71a1aafdcb5ac9f..e89752798631dff69797584e2be86e680904bf9b 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -120,7 +120,7 @@ object Definitions {
       case PackageImport(pack) => {
         import DefOps._
         // Ignore standalone modules, assume there are extra imports for them
-        unitsInPackage(inProgram(this),pack) 
+        inProgram(this) map { unitsInPackage(_,pack) } getOrElse List()
       }
       case SingleImport(imported) => List(imported)
       case WildcardImport(imported) => imported.subDefinitions
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index cb13003325abfd90366ad18f437156733b2d5b93..2e9b0a4204dbf609dc1a80a9f700370a9716bfee 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -2194,7 +2194,9 @@ object TreeOps {
 
   def isStringLiteral(e: Expr): Option[String] = e match {
     case CaseClass(cct, args) =>
-      val lib = inProgram(cct.classDef).library
+      val p = inProgram(cct.classDef)
+      require(p.isDefined)
+      val lib = p.get.library
 
       if (Some(cct.classDef) == lib.String) {
         isListLiteral(args(0)) match {
@@ -2222,7 +2224,9 @@ object TreeOps {
 
   def isListLiteral(e: Expr): Option[(TypeTree, List[Expr])] = e match {
     case CaseClass(cct, args) =>
-      val lib = inProgram(cct.classDef).library
+      val p = inProgram(cct.classDef)
+      require(p.isDefined)
+      val lib = p.get.library
 
       if (Some(cct.classDef) == lib.Nil) {
         Some((cct.tps.head, Nil))