diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index a5d0deb5d96f641954de045bdb8b4cb9cda85faa..156c0dd5cf299b32ebf458b63eba61b2c78bebd5 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -498,7 +498,7 @@ trait CodeExtraction extends ASTExtractors {
               Some(AbstractClassType(acd, newTps))
 
             case cd =>
-              outOfSubsetError(sym.pos, "Class "+id+" cannot extend "+cd.id)
+              outOfSubsetError(sym.pos, s"Class $id cannot extend ${cd.id}")
               None
           }
 
@@ -506,28 +506,15 @@ trait CodeExtraction extends ASTExtractors {
           None
       }
 
-      val cd = if (sym.isAbstractClass) {
-        val acd = AbstractClassDef(id, tparams, parent).setPos(sym.pos)
-
-        classesToClasses += sym -> acd
-        parent.foreach(_.classDef.registerChild(acd))
-        acd.addFlags(annotationsOf(sym).map { case (name, args) => ClassFlag.fromName(name, args) }.toSet)
-      } else {
-        val ccd = CaseClassDef(id, tparams, parent, sym.isModuleClass).setPos(sym.pos)
-        classesToClasses += sym -> ccd
-        parent.foreach(_.classDef.registerChild(ccd))
-        ccd.addFlags(annotationsOf(sym).map { case (name, args) => ClassFlag.fromName(name, args) }.toSet)
-
-        val fields = args.map { case (fsym, t) =>
-          val tpe = leonType(t.tpt.tpe)(defCtx, fsym.pos)
-          val id = overridenOrFresh(fsym, Some(ccd), tpe)
-          LeonValDef(id.setPos(t.pos), Some(tpe)).setPos(t.pos)
-        }
-
-        ccd.setFields(fields)
-
-        ccd
-      }
+      val cd = ( if (sym.isAbstractClass) {
+        AbstractClassDef(id, tparams, parent)
+      } else  {
+        CaseClassDef(id, tparams, parent, sym.isModuleClass)
+      }).setPos(sym.pos)
+      classesToClasses += sym -> cd
+      //println(s"Registering $sym")
+      parent.foreach(_.classDef.registerChild(cd))
+      cd.addFlags(annotationsOf(sym).map { case (name, args) => ClassFlag.fromName(name, args) }.toSet)
 
       // Validates type parameters
       parent foreach { pct =>
@@ -558,19 +545,19 @@ trait CodeExtraction extends ASTExtractors {
 
         // Normal methods
         case t @ ExFunctionDef(fsym, _, _, _, _) =>
+          isMethod += fsym
           val fd = defineFunDef(fsym, Some(cd))(defCtx)
 
-          isMethod += fsym
+
           methodToClass += fd -> cd
 
           cd.registerMethod(fd)
 
         // Default values for parameters
         case t@ ExDefaultValueFunction(fsym, _, _, _, owner, index, _) =>
+          isMethod += fsym
           val fd = defineFunDef(fsym)(defCtx)
           fd.addFlag(IsSynthetic)
-
-          isMethod += fsym
           methodToClass += fd -> cd
 
           cd.registerMethod(fd)
@@ -581,9 +568,8 @@ trait CodeExtraction extends ASTExtractors {
 
         // Lazy fields
         case t @ ExLazyAccessorFunction(fsym, _, _)  =>
-          val fd = defineFieldFunDef(fsym, true, Some(cd))(defCtx)
-
           isMethod += fsym
+          val fd = defineFieldFunDef(fsym, true, Some(cd))(defCtx)
           methodToClass += fd -> cd
 
           cd.registerMethod(fd)
@@ -591,11 +577,9 @@ trait CodeExtraction extends ASTExtractors {
         // normal fields
         case t @ ExFieldDef(fsym, _, _) =>
           //println(fsym + "matched as ExFieldDef")
-          // we will be using the accessor method of this field everywhere 
-          val fsymAsMethod = fsym
-          val fd = defineFieldFunDef(fsymAsMethod, false, Some(cd))(defCtx)
-
-          isMethod += fsymAsMethod
+          // we will be using the accessor method of this field everywhere
+          isMethod += fsym
+          val fd = defineFieldFunDef(fsym, false, Some(cd))(defCtx)
           methodToClass += fd -> cd
 
           cd.registerMethod(fd)
@@ -604,6 +588,19 @@ trait CodeExtraction extends ASTExtractors {
 
       }
 
+      cd match {
+        case ccd: CaseClassDef =>
+
+          val fields = args.map { case (fsym, t) =>
+            val tpe = leonType(t.tpt.tpe)(defCtx, fsym.pos)
+            val id = overridenOrFresh(fsym, Some(ccd), tpe)
+            LeonValDef(id.setPos(t.pos), Some(tpe)).setPos(t.pos)
+          }
+          //println(s"Fields of $sym")
+          ccd.setFields(fields)
+        case _ =>
+      }
+
       cd
     }
 
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 6d020cc710bb5cf5dca8eda06dc4500163edf95a..02acab8d15ff0e60aaa507392f765501563cc3ee 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -402,7 +402,7 @@ class PrettyPrinter(opts: PrinterOptions,
 
       // Definitions
       case Program(units) =>
-        p"""${nary(units, "\n\n")}"""
+        p"""${nary(units filter { _.isMainUnit }, "\n\n")}"""
 
       case UnitDef(id,pack, imports, defs,_) =>
         if (pack.nonEmpty){