Improve FunDef.duplicate. FunDef.copyContentFrom

src/main/scala/leon/purescala/Definitions.scala

@@ -212,10 +212,15 @@ object Definitions {
 
     def duplicate: FunDef = {
       val fd = new FunDef(id, tparams, returnType, params)
-      fd.fullBody = fullBody
-      fd.parent = parent
-      fd.orig = orig
-      fd
+      fd.copyContentFrom(this)
+      fd.copiedFrom(this)
+    }
+    
+    def copyContentFrom(from : FunDef) {
+      this.fullBody       = from.fullBody
+      this.parent         = from.parent
+      this.orig           = from.orig
+      this.addAnnotation(from.annotations.toSeq : _*)
     }
 
     def hasBody                     = body.isDefined

src/main/scala/leon/purescala/MethodLifting.scala

@@ -30,12 +30,8 @@ object MethodLifting extends TransformationPhase {
         val receiver = FreshIdentifier("$this").setType(recType).setPos(cd.id)
 
         val nfd = new FunDef(id, ctParams ++ fd.tparams, fd.returnType, ValDef(receiver, recType) +: fd.params)
-        nfd.postcondition = fd.postcondition
-        nfd.precondition  = fd.precondition
-        nfd.body          = fd.body
-
+        nfd.copyContentFrom(fd)
         nfd.setPos(fd)
-        nfd.addAnnotation(fd.annotations.toSeq : _*)
 
         mdToFds += fd -> nfd
       }