diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index 4c27e9b96ca6d7cdbd3795d9cfb8285561e9212c..543b377843d77372fbce8151337f3a6b09390c94 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -80,10 +80,13 @@ object ConvertHoles extends LeonPhase[Program, Program] {
 
           val choose = Choose(spec)
 
+          val newBody = if (holes.size == 1) {
+            replaceFromIDs(Map(holes.head -> choose), withoutHoles)
+          } else {
+            letTuple(holes, choose, withoutHoles)
+          }
 
-          val valuations = letTuple(holes, choose, withoutHoles)
-
-          withPostcondition(withPrecondition(valuations, pre), post)
+          withPostcondition(withPrecondition(newBody, pre), post)
 
         } else {
           e
@@ -93,7 +96,7 @@ object ConvertHoles extends LeonPhase[Program, Program] {
     }
   }
 
-   
+
   def run(ctx: LeonContext)(pgm: Program): Program = {
     pgm.definedFunctions.foreach(fd => fd.fullBody = convertHoles(fd.fullBody,ctx) )
     pgm