diff --git a/src/main/scala/leon/grammars/FunctionCalls.scala b/src/main/scala/leon/grammars/FunctionCalls.scala
index 1233fb1931a83b5ca674019be0c85144339dd19f..65836341ea95ccfd9bb302faf279bbc5b7bdc4a9 100644
--- a/src/main/scala/leon/grammars/FunctionCalls.scala
+++ b/src/main/scala/leon/grammars/FunctionCalls.scala
@@ -63,8 +63,7 @@ case class FunctionCalls(prog: Program, currentFunction: FunDef, types: Seq[Type
                  }
                }
              } else {
-               /* All type parameters that used to be free are assigned
-                */
+               // All type parameters that used to be free are assigned
                List(tfd)
              }
            case None =>
@@ -75,7 +74,7 @@ case class FunctionCalls(prog: Program, currentFunction: FunDef, types: Seq[Type
        }
      }
 
-     val filter = (tfd:TypedFunDef) => tfd.fd.isSynthetic || (exclude contains tfd.fd)
+     val filter = (tfd:TypedFunDef) => tfd.fd.isSynthetic || tfd.fd.isInner || (exclude contains tfd.fd)
      val funcs = visibleFunDefsFromMain(prog).toSeq.sortBy(_.id).flatMap(getCandidates).filterNot(filter)
 
      funcs.map{ tfd =>
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 753e9236064a4ee3eaedbe13647de85a133dcd5f..2178a07af2ea4a0d88d1209a4b2eebedfc299f19 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -190,6 +190,13 @@ object Definitions {
     }
   }
 
+  /** A trait that represents flags that annotate a ClassDef with different attributes */
+  sealed trait ClassFlag
+
+  object ClassFlag {
+    def fromName(name: String, args: Seq[Option[Any]]): ClassFlag = Annotation(name, args)
+  }
+
   /** A trait that represents flags that annotate a FunDef with different attributes */
   sealed trait FunctionFlag
 
@@ -200,13 +207,6 @@ object Definitions {
     }
   }
 
-  /** A trait that represents flags that annotate a ClassDef with different attributes */
-  sealed trait ClassFlag
-
-  object ClassFlag {
-    def fromName(name: String, args: Seq[Option[Any]]): ClassFlag = Annotation(name, args)
-  }
-
   // Whether this FunDef was originally a (lazy) field
   case class IsField(isLazy: Boolean) extends FunctionFlag
   // Compiler annotations given in the source code as @annot
@@ -224,6 +224,7 @@ object Definitions {
   case object IsInlined extends FunctionFlag
   // Is an ADT invariant method
   case object IsADTInvariant extends FunctionFlag with ClassFlag
+  case object IsInner extends FunctionFlag
 
   /** Represents a class definition (either an abstract- or a case-class) */
   sealed trait ClassDef extends Definition {
@@ -357,7 +358,7 @@ object Definitions {
     ): AbstractClassDef = {
       val acd = new AbstractClassDef(id, tparams, parent)
       acd.addFlags(this.flags)
-      parent.map(_.classDef.ancestors.map(_.registerChild(acd)))
+      parent.foreach(_.classDef.ancestors.foreach(_.registerChild(acd)))
       acd.copiedFrom(this)
     }
   }
@@ -398,7 +399,7 @@ object Definitions {
     def typed: CaseClassType = typed(tparams.map(_.tp))
     
     /** Duplication of this [[CaseClassDef]].
-      * @note This will not replace recursive case class def calls in [[arguments]] nor the parent abstract class types
+      * @note This will not replace recursive [[CaseClassDef]] calls in [[fields]] nor the parent abstract class types
       */
     def duplicate(
       id: Identifier                    = this.id.freshen,
@@ -411,7 +412,7 @@ object Definitions {
       cd.setFields(fields)
       cd.addFlags(this.flags)
       cd.copiedFrom(this)
-      parent.map(_.classDef.ancestors.map(_.registerChild(cd)))
+      parent.foreach(_.classDef.ancestors.foreach(_.registerChild(cd)))
       cd
     }
   }
@@ -506,6 +507,7 @@ object Definitions {
     def isRealFunction    = !canBeField
     def isSynthetic       = flags contains IsSynthetic
     def isInvariant       = flags contains IsADTInvariant
+    def isInner           = flags contains IsInner
     def methodOwner       = flags collectFirst { case IsMethod(cd) => cd }
 
     /* Wrapping in TypedFunDef */
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 07c6781a8389be1df4e16681cd518bb043cb608a..ff8feb33edc440a876cd0ad506b0e0da92967bb2 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -8,8 +8,8 @@ import Expressions._
 import ExprOps._
 import Constructors._
 import TypeOps.instantiateType
-import leon.purescala.Common.Identifier
-import leon.purescala.Types.TypeParameter
+import Common.Identifier
+import Types.TypeParameter
 import utils.GraphOps._
 
 object FunctionClosure extends TransformationPhase {
@@ -108,6 +108,7 @@ object FunctionClosure extends TransformationPhase {
     }
 
     val funs = closed.values.toSeq.map{ _.newFd }
+    funs foreach (_.addFlag(IsInner))
 
     // Recursively close new functions
     fd +: funs.flatMap(close)