diff --git a/library/collection/List.scala b/library/collection/List.scala
index 8ee7c398aa09d684ebf6a6cfb1f51124d4451151..74a0f0c66e3bc23780076e16acdc6f7035c6986b 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -556,11 +556,9 @@ sealed abstract class List[T] {
 }
 
 @isabelle.constructor(name = "List.list.Cons")
-@library
 case class Cons[T](h: T, t: List[T]) extends List[T]
 
 @isabelle.constructor(name = "List.list.Nil")
-@library
 case class Nil[T]() extends List[T]
 
 object List {
diff --git a/library/lang/Option.scala b/library/lang/Option.scala
index 04412e51b7b8cf642d6cc1d237e76f5b2907c8cf..a6f09db68f3fecc7ad8095506a49d21e4d8ac7ad 100644
--- a/library/lang/Option.scala
+++ b/library/lang/Option.scala
@@ -78,9 +78,7 @@ sealed abstract class Option[T] {
 }
 
 @isabelle.constructor(name = "Option.option.Some")
-@library
 case class Some[T](v: T) extends Option[T]
 
 @isabelle.constructor(name = "Option.option.None")
-@library
 case class None[T]() extends Option[T]
diff --git a/library/lang/package.scala b/library/lang/package.scala
index 679495565b674ce4d0869d9082cff1a3a2b3c764..b19ec529bdb3975956de00a7da8e8ad39bcf34e4 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -8,7 +8,6 @@ import scala.language.implicitConversions
 package object lang {
 
   implicit class BooleanDecorations(val underlying: Boolean) {
-
     @inline
     def holds : Boolean = {
       underlying
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index cb0c7f96f914c190954a3c896ef531efe127bb8f..67e5c4502ad1810b323616916e3edfab9c05a8ea 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -453,11 +453,7 @@ trait ASTExtractors {
           } else if (!dd.symbol.isSynthetic) {
             Some((dd.symbol, tparams.map(_.symbol), vparamss.flatten, tpt.tpe, rhs))
           } else {
-            if(name.toString == "copy" || name.toString.startsWith("copy$default$")) {
-              Some((dd.symbol, tparams.map(_.symbol), vparamss.flatten, tpt.tpe, rhs))
-            } else {
-              None
-            }
+            None
           }
         case _ => None
       }
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 40091637c3c9dfa019df83a1b502448b7b221881..8fb753d23d35364059115f7032bef3310c492d82 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -351,21 +351,6 @@ object Definitions {
       CaseClassType(this, tps)
     }
     def typed: CaseClassType = typed(tparams.map(_.tp))
-
-    //TODO: the function works via a horrible hack, as it is not very clear where the
-    //      companion object will end up being defined.
-    //      This also return an Option as Leon compiles some non-case class (so without
-    //      copy) towards an internal case class.
-    //FIXME: it does not properly handle copy methods coming from multiple children
-    //       that got lifted to a single root class.
-    def copyDef(implicit pgm: Program): Option[FunDef] = {
-      val tryName1 = DefOps.fullName(this.root) + ".copy"
-      val tryName2 = this.root.id.name + ".copy" //generated companion object of case classes defined inside objects are currently lifted at the top level.
-      pgm.lookup(tryName1).collectFirst { case (fd: FunDef) => fd }.orElse(
-        pgm.lookup(tryName2).collectFirst { case (fd: FunDef) => fd }
-      )
-    }
-
   }
 
   /** Function/method definition.
diff --git a/src/test/resources/regression/verification/purescala/valid/Copy.scala b/src/test/resources/regression/verification/purescala/valid/Copy.scala
deleted file mode 100644
index d30d403a0be0dc9257653f2c4b817c3c8e0d2016..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/verification/purescala/valid/Copy.scala
+++ /dev/null
@@ -1,16 +0,0 @@
-object Copy {
-
-  case class A(a: Int, b: Int)
-
-  def f(a: A): A = {
-    a.copy(b = 17)
-  } ensuring(res => res.a == a.a && res.b == 17)
-
-  def g(a: A): A = {
-    a.copy(b = 17)
-  } ensuring(res => res.a == a.a)
-
-  def h(a: A): A = {
-    a.copy(b = 17)
-  } ensuring(res => res.b == 17)
-}