diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 21359f8ba7622c1f21ab6f71dbd50f524138fc01..9f56f7ba1fcf3d190a5e9d37f529acdc580a44b2 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -84,10 +84,6 @@ object Definitions {
       case ccd: CaseClassDef if ccd.id.name == name => ccd
     }.headOption.getOrElse(throw LeonFatalError("Unknown case class '"+name+"'"))
 
-    def duplicate = {
-      copy(units = units.map{_.duplicate})
-    }
-    
     def lookupAll(name: String)  = DefOps.searchWithin(name, this)
     def lookup(name: String)     = lookupAll(name).headOption
   }
@@ -174,14 +170,6 @@ object Definitions {
       }
     }
 
-    def duplicate = {
-      copy(defs = defs map {
-        case cd: ClassDef => cd.duplicate
-        case m: ModuleDef => m.duplicate
-        case d => d
-      })
-    }
-
     def modules = defs.collect {
       case md: ModuleDef => md
     }
@@ -213,12 +201,7 @@ object Definitions {
     lazy val singleCaseClasses : Seq[CaseClassDef] = defs.collect {
       case c @ CaseClassDef(_, _, None, _) => c
     }
-    
-    def duplicate = copy(defs = defs map {
-      case f: FunDef => f.duplicate
-      case cd: ClassDef => cd.duplicate
-      case other => other
-    })
+
   }
 
   /** Useful because case classes and classes are somewhat unified in some
@@ -271,26 +254,11 @@ object Definitions {
 
     val isAbstract: Boolean
     val isCaseObject: Boolean
-    
-    def duplicate = this match {
-      case ab : AbstractClassDef => {
-        val ab2 = ab.copy()
-        ab.knownChildren foreach ab2.registerChildren
-        ab.methods foreach { m => ab2.registerMethod(m.duplicate) }
-        ab2
-      }
-      case cc : CaseClassDef => {
-        val cc2 = cc.copy() 
-        cc.methods foreach { m => cc2.registerMethod(m.duplicate) }
-        cc2.setFields(cc.fields map { _.copy() })
-        cc2
-      }
-    }
-    
+
     lazy val definedFunctions : Seq[FunDef] = methods
     lazy val definedClasses = Seq(this)
     lazy val classHierarchyRoots = if (this.hasParent) Seq(this) else Nil
-    
+
   }
 
   /** Abstract classes. */
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 2b2b2b36976703d1c8f268af0e9558e64461e555..b156a4bde8b102ee148dd2cbb4774868d7fc5480 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1933,9 +1933,7 @@ object ExprOps {
     import synthesis.Witnesses.Terminating
     val res1 = preMap({
       case LetDef(fd, b) =>
-        val nfd = new FunDef(fd.id.freshen, fd.tparams, fd.returnType, fd.params)
-        nfd.copyContentFrom(fd)
-        nfd.copiedFrom(fd)
+        val nfd = fd.duplicate
 
         fds += fd -> nfd
 
diff --git a/src/main/scala/leon/purescala/RestoreMethods.scala b/src/main/scala/leon/purescala/RestoreMethods.scala
index bd6a51cd00c082d363380f217faabe4a9226ff9b..cedc3a4378c468084c935e3afb3953602c9ae686 100644
--- a/src/main/scala/leon/purescala/RestoreMethods.scala
+++ b/src/main/scala/leon/purescala/RestoreMethods.scala
@@ -43,14 +43,11 @@ object RestoreMethods extends TransformationPhase {
     // We inject methods, 
     def processClassDef(cd: ClassDef): ClassDef = {
       if (classMethods contains cd) {
-        val ncd = cd.duplicate
         for (md <- classMethods(cd).map(fdToMd)) {
-          ncd.registerMethod(md)
+          cd.registerMethod(md)
         }
-        ncd
-      } else {
-        cd
       }
+      cd
     }
 
     val np = p.copy(units = p.units.map { u =>