diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index 60a6f8ea0bf1e4b2346c98085699fa7a8b9d228c..be878918adf52bc0f3281a4dfada1055b256c533 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -8,6 +8,7 @@ import purescala.Trees._
 import purescala.TypeTrees._
 import purescala.TreeOps._
 import purescala.Definitions._
+import purescala.Constructors._
 
 object ConvertHoles extends LeonPhase[Program, Program] {
   val name        = "Convert Holes to Choose"
@@ -62,11 +63,7 @@ object ConvertHoles extends LeonPhase[Program, Program] {
               BooleanLiteral(true)
           }
 
-          val withChoose = if (holes.size > 1) {
-            LetTuple(holes, Choose(cids, pred), newBody)
-          } else {
-            Let(holes.head, Choose(cids, pred), newBody)
-          }
+          val withChoose = letTuple(holes, Choose(cids, pred), newBody)
 
           fd.body = Some(withChoose)
         }
diff --git a/src/main/scala/leon/synthesis/ConvertWithOracles.scala b/src/main/scala/leon/synthesis/ConvertWithOracles.scala
index d7c1b6853d7c554b656983c1aabb2f58a08f098b..f8072b71a9dedfd1ff50e705607d1f24b1789b57 100644
--- a/src/main/scala/leon/synthesis/ConvertWithOracles.scala
+++ b/src/main/scala/leon/synthesis/ConvertWithOracles.scala
@@ -7,6 +7,7 @@ import purescala.Common._
 import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Definitions._
+import purescala.Constructors._
 
 object ConvertWithOracle extends LeonPhase[Program, Program] {
   val name        = "Convert WithOracle to Choose"
@@ -53,11 +54,7 @@ object ConvertWithOracle extends LeonPhase[Program, Program] {
                     BooleanLiteral(true)
                 }
 
-                if (chooseOs.size > 1) {
-                  Some(LetTuple(os, Choose(chooseOs, pred), b))
-                } else {
-                  Some(Let(os.head, Choose(chooseOs, pred), b))
-                }
+                Some(letTuple(os, Choose(chooseOs, pred), b))
               case None =>
                 None
             }
diff --git a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
index a042753a64e543cbe842cc0bf07dfeaa5c1c307d..f64f3f31bc12861696911a3cb4787f55868fec66 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
@@ -10,6 +10,7 @@ import purescala.Common._
 import purescala.TypeTrees._
 import purescala.TreeOps._
 import purescala.Extractors._
+import purescala.Constructors._
 
 case object DetupleOutput extends Rule("Detuple Out") {
 
@@ -39,13 +40,12 @@ case object DetupleOutput extends Rule("Detuple Out") {
       }.unzip
 
       val newOuts = subOuts.flatten
-      //sctx.reporter.warning("newOuts: " + newOuts.toString)
 
       val sub = Problem(p.as, p.pc, subProblem, newOuts)
 
       val onSuccess: List[Solution] => Option[Solution] = {
         case List(sol) =>
-          Some(Solution(sol.pre, sol.defs, LetTuple(newOuts, sol.term, Tuple(outerOuts))))
+          Some(Solution(sol.pre, sol.defs, letTuple(newOuts, sol.term, Tuple(outerOuts))))
         case _ =>
           None
       }
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index 7deff8fe62a2df6ed1d0d91935251edb0795097d..39286e3c14ede675c56e4fd1842347cacb3d51e5 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -8,6 +8,7 @@ import purescala.Common._
 import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Extractors._
+import purescala.Constructors._
 
 case object OnePoint extends NormalizingRule("One-point") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
@@ -32,14 +33,9 @@ case object OnePoint extends NormalizingRule("One-point") {
 
       val newProblem = Problem(p.as, p.pc, subst(x -> e, And(others)), oxs)
 
-      val onSuccess: List[Solution] => Option[Solution] = { 
+      val onSuccess: List[Solution] => Option[Solution] = {
         case List(Solution(pre, defs, term)) =>
-          if (oxs.isEmpty) {
-            Some(Solution(pre, defs, Tuple(e :: Nil)))
-          } else {
-            Some(Solution(pre, defs, LetTuple(oxs, term, subst(x -> e, Tuple(p.xs.map(Variable(_)))))))
-          }
-
+          Some(Solution(pre, defs, letTuple(oxs, term, subst(x -> e, Tuple(p.xs.map(Variable(_)))))))
         case _ =>
           None
       }
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index 1e5a3a3318e3ac3f9b3d050bbd81fa81395514e4..b349279c5b31a8ab9172ed67314c6bf6c11a9279 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -7,6 +7,7 @@ package rules
 import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Extractors._
+import purescala.Constructors._
 
 case object UnconstrainedOutput extends NormalizingRule("Unconstr.Output") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
@@ -17,13 +18,8 @@ case object UnconstrainedOutput extends NormalizingRule("Unconstr.Output") {
 
       val onSuccess: List[Solution] => Option[Solution] = { 
         case List(s) =>
-          val term = if (sub.xs.size > 1) {
-            LetTuple(sub.xs, s.term, Tuple(p.xs.map(id => if (unconstr(id)) simplestValue(id.getType) else Variable(id))))
-          } else if (sub.xs.size == 1) {
-            Let(sub.xs.head, s.term, Tuple(p.xs.map(id => if (unconstr(id)) simplestValue(id.getType) else Variable(id))))
-          } else {
-            Tuple(p.xs.map(id => simplestValue(id.getType)))
-          }
+          val term = letTuple(sub.xs, s.term, Tuple(p.xs.map(id => if (unconstr(id)) simplestValue(id.getType) else Variable(id))))
+
           Some(Solution(s.pre, s.defs, term))
         case _ =>
           None