diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 0540745f193243f55b0330749cf757f3cba94933..f83c724dbcbc52e8f44c29a2d35d7b5a52638c55 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -672,9 +672,6 @@ trait CodeGeneration {
         ch << InvokeSpecial(ErrorClass, constructorName, "(Ljava/lang/String;)V")
         ch << ATHROW
 
-      case rh: RepairHole =>
-        mkExpr(simplestValue(rh.getType), ch) // It is expected to be invalid, we want to repair it
-
       case Choose(_, _, Some(e)) =>
         mkExpr(e, ch)
 
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 747a5d52b6a62a8cfa002537b4aa2b71ea968b93..6eb4323b46271846625b2ed6116a33cf6a7bbace 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -393,9 +393,6 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
     case gv: GenericValue =>
       gv
 
-    case rh: RepairHole =>
-      simplestValue(rh.getType) // It will be wrong, we don't care
-
     case g : Gives =>
       e(convertHoles(g, ctx, true)) 
   
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index a7b5f1e87e37c71d8041c27a70dbda3e197506c2..0424350cf2ae76a1f4e1a9b08d3c95faa156e484 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -421,16 +421,6 @@ trait ASTExtractors {
       }
     }
 
-    object ExRepairHoleExpression {
-      def unapply(tree: Tree) : Option[(Tree, List[Tree])] = tree match {
-        case a @ Apply(TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "$qmark$bang"), List(tpt)), args1)  =>
-            Some((tpt, args1))
-        case TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "$qmark$bang"), List(tpt)) =>
-            Some((tpt, Nil))
-        case _ => None
-      }
-    }
-
     object ExHoleExpression {
       def unapply(tree: Tree) : Option[(Tree, List[Tree])] = tree match {
         case a @ Apply(TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "$qmark"), List(tpt)), args1)  =>
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index b98faa52f1e0ffd27bb43d53998d8f206c5a9e4c..bbfffc373a027c8f798d3451f1d1630ccf66037a 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1229,11 +1229,6 @@ trait CodeExtraction extends ASTExtractors {
 
           Hole(extractType(tpt), exprs.map(extractTree))
 
-        case hole @ ExRepairHoleExpression(tpt, exprs) =>
-          val leonExprs = exprs.map(extractTree)
-
-          RepairHole(extractType(tpt), exprs.map(extractTree))
-
         case ops @ ExWithOracleExpression(oracles, body) =>
           val newOracles = oracles map { case (tpt, sym) =>
             val aTpe  = extractType(tpt)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index fa16449fac0b5e37cc9b232990b0a4a321989aef..de7052e2237ab99b8f234408e92966bcf251b342 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -240,9 +240,6 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
             |  $pred
             |}"""
 
-      case h @ RepairHole(tpe, es) =>
-        p"""|?![$tpe]($es)"""
-
       case h @ Hole(tpe, es) =>
         if (es.isEmpty) {
           p"""|???[$tpe]"""
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index ebba57547887f478615193f3b1e8de6950018395..801469a6bd5c250ebedf241bddaba0424e97de80 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1409,7 +1409,6 @@ object TreeOps {
     preTraversal{
       case Choose(_, _, None) => return false
       case Hole(_, _) => return false
-      case RepairHole(_, _) => return false
       case Gives(_,_) => return false
       case _ =>
     }(e)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 421d97600d994c5d513537c26714338fd4407104..052dd2305c89cee209e1a9d0ce783b15fcdb5c3c 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -477,14 +477,6 @@ object Trees {
     }
   }
 
-  case class RepairHole(tpe: TypeTree, components: Seq[Expr]) extends Expr with NAryExtractable {
-    val getType = tpe
-
-    def extract = {
-      Some((components, (es: Seq[Expr]) => RepairHole(tpe, es).setPos(this)))
-    }
-  }
-
   /**
    * DEPRECATED TREES
    * These trees are not guaranteed to be supported by Leon.
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index cdad71b8859c2dcb0e2be28f778f9234a3be3bf3..a570d95977008edb2e087897cfa61d95c34e2b88 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -264,15 +264,9 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
           }
         }
 
-        case h @ RepairHole(_, _) =>
-          val hid = FreshIdentifier("hole", true).setType(h.getType)
-          exprVars += hid
-          Variable(hid)
-
         case c @ Choose(ids, cond, Some(impl)) =>
           rec(pathVar, impl)
 
-
         case c @ Choose(ids, cond, None) =>
           val cid = FreshIdentifier("choose", true).setType(c.getType)
           storeExpr(cid)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 51dc20d565bb58e70573a26cb744fec0cbd1cc5a..02b6683c4360e5261446cca4d5ae30b191428a90 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -676,11 +676,6 @@ trait AbstractZ3Solver
       case gv @ GenericValue(tp, id) =>
         z3.mkApp(genericValueToDecl(gv))
 
-      case h @ RepairHole(_, _) =>
-        val newAST = z3.mkFreshConst("hole", typeToSort(h.getType))
-        variables += (h -> newAST)
-        newAST
-
       case _ => {
         reporter.warning(ex.getPos, "Can't handle this in translation to Z3: " + ex)
         throw new CantTranslateException