diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 61b8c53a6c5ae143149b695ae167b781651c89b0..779aad137c1b18d7d13451b6cd2da3fc1d50275b 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -351,6 +351,9 @@ object Definitions {
     val defType : DefType
   ) extends Definition {
     
+    // A copy of the original function before Xlang elimination
+    var orig : Option[FunDef] = None
+    
     private var fullBody_ : Expr = NoTree(returnType)
     def fullBody = fullBody_
     def fullBody_= (e : Expr) {
@@ -385,8 +388,7 @@ object Definitions {
     
     def copyContentFrom(from : FunDef) {
       this.fullBody  = from.fullBody 
-      //this.parent   = from.parent
-      //this.orig    = from.orig
+      this.orig    = from.orig
       this.origOwner = from.origOwner
       this.addAnnotation(from.annotations.toSeq : _*)
     }
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 7d9066f895fb9bcc841b2ad005127aac29d97188..c80deca872fa16478af39fbea0d2f30b6a4b8330 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -64,7 +64,7 @@ object FunctionClosure extends TransformationPhase {
       newFunDef.addAnnotation(fd.annotations.toSeq:_*) //TODO: this is still some dangerous side effects
       newFunDef.setOwner(parent)
       fd       .setOwner(parent)
-      newFunDef.origOwner   = Some(fd)
+      newFunDef.orig = Some(fd)
 
       def introduceLets(expr: Expr, fd2FreshFd: Map[FunDef, (FunDef, Seq[Variable])]): Expr = {
         val (newExpr, _) = enclosingLets.foldLeft((expr, Map[Identifier, Identifier]()))((acc, p) => {
diff --git a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala b/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
index 3ec56711560a4a2e3750a729410950bccd292fbf..03c8d2e71c079afbeceaf76ef2e97eb4e3bb45e9 100644
--- a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
@@ -21,8 +21,8 @@ object XlangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
     val (pgm3, wasLoop) = ImperativeCodeElimination.run(ctx)(pgm2)
     val pgm4 = purescala.FunctionClosure.run(ctx)(pgm3)
 
-    def functionWasLoop(fd: FunDef): Boolean = fd.origOwner match {
-      case Some(nested : FunDef) => // was a nested function
+    def functionWasLoop(fd: FunDef): Boolean = fd.orig match {
+      case Some(nested) => // could have been a LetDef originally
         wasLoop.contains(nested)
       case _ => false //meaning, this was a top level function
     }