diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 0d096025a2b359e63fcb780cc8249883b4bb04b1..678305670feb63f25720a9428608bedf846b66e6 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -379,8 +379,8 @@ object ExprOps {
   /** Returns functions in directly nested LetDefs */
   def directlyNestedFunDefs(e: Expr): Set[FunDef] = {
     fold[Set[FunDef]]{
-      case (LetDef(fds,_), Seq(fromFds, fromBd)) => fromBd ++ fds
-      case (_, subs) => subs.flatten.toSet
+      case (LetDef(fds,_), fromFdsFromBd) => fromFdsFromBd.last ++ fds
+      case (_,             subs) => subs.flatten.toSet
     }(e)
   }
 
@@ -2142,7 +2142,7 @@ object ExprOps {
 
     // we now remove LetDefs
     val res2 = preMap({
-      case LetDef(fd, b) =>
+      case LetDef(fds, b) =>
         Some(b)
       case _ =>
         None
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 0a62d8e0334841f8a54e3829cf46abba7282f404..0c18b51e3b9e473556aaf5817b49ad0d8104ea40 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -62,7 +62,7 @@ object FunctionClosure extends TransformationPhase {
 
     // Remove LetDefs from fd
     fd.fullBody = preMap({
-      case LetDef(fd, bd) =>
+      case LetDef(fds, bd) =>
         Some(bd)
       case _ =>
         None
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 89b58f83ce45af7ee5845def6ae0dff636d6967b..b7372ba044d89e294c829c1149e5ef05ada7014a 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -89,9 +89,11 @@ class PrettyPrinter(opts: PrinterOptions,
           p"""|val $b = $d
               |$e"""
 
-      case LetDef(fd,body) =>
-        p"""|$fd
-            |$body"""
+      case LetDef(a::q,body) =>
+        p"""|$a
+            |${LetDef(q, body)}"""
+      case LetDef(Nil,body) =>
+        p"""$body"""
 
       case Require(pre, body) =>
         p"""|require($pre)
@@ -625,6 +627,7 @@ class PrettyPrinter(opts: PrinterOptions,
     case (e: Expr, _) if isSimpleExpr(e) => false
     case (e: Expr, Some(within: Expr)) if noBracesSub(within) contains e => false
     case (_: Expr, Some(_: MatchCase)) => false
+    case (_: LetDef, Some(_: LetDef)) => false
     case (e: Expr, Some(_)) => true
     case _ => false
   }
diff --git a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
index 109cd677db133e962f4d0ece64794e38ab38b8e7..42e3e6d99bb5cd804ff753f9d32225c63196898b 100644
--- a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
@@ -40,7 +40,7 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
               } }
               if(i == -1) {
                 fd.postcondition = Some(Lambda(Seq(ValDef(id, tpe)), and(post, Passes(inputVariables, Variable(id), newCases))))
-                ctx0.reporter.info("No top-level passes in postcondition, adding it:  " + fd)
+                //ctx0.reporter.info("No top-level passes in postcondition, adding it:  " + fd)
               } else {
                 val newPasses = exprs(i) match {
                   case Passes(in, out, cases) =>
@@ -49,17 +49,17 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
                 }
                 val newPost = and(exprs.updated(i, newPasses) : _*)
                 fd.postcondition = Some(Lambda(Seq(ValDef(id, tpe)), newPost))
-                ctx0.reporter.info("Adding the example to the passes postcondition: " + fd)
+                //ctx0.reporter.info("Adding the example to the passes postcondition: " + fd)
               }
           }
         } else {
           fd.postcondition = Some(Lambda(Seq(ValDef(id, tpe)), and(post, Passes(inputVariables, Variable(id), newCases))))
-          ctx0.reporter.info("No passes in postcondition, adding it:" + fd)
+          //ctx0.reporter.info("No passes in postcondition, adding it:" + fd)
         }
       case None =>
         val id = FreshIdentifier("res", fd.returnType, false)
         fd.postcondition = Some(Lambda(Seq(ValDef(id, None)), Passes(inputVariables, Variable(id), newCases)))
-        ctx0.reporter.info("No postcondition, adding it: " + fd)
+        //ctx0.reporter.info("No postcondition, adding it: " + fd)
     }
     fd.body match { // TODO: Is it correct to discard the choose construct inside the body?
       case Some(Choose(Lambda(Seq(ValDef(id, tpe)), bodyChoose))) => fd.body = Some(Hole(id.getType, Nil))
diff --git a/testcases/stringrender/GrammarRender.scala b/testcases/stringrender/GrammarRender.scala
index f0c1e5929f2bd9a3866b288e48eed96c35968fc6..a2de93e9b41bc552db923b9eec2cce3fdf89d41b 100644
--- a/testcases/stringrender/GrammarRender.scala
+++ b/testcases/stringrender/GrammarRender.scala
@@ -182,9 +182,6 @@ S0 -> S0 t1"""
     }
     "(" + renderSymbol(s.start) + ", [" + renderListRules(s.rules) + "])"
   } ensuring psHTMLRules(s)
-
-  case Grammar(NonTerminal(0), Cons(Rule(NonTerminal(0), Cons(Terminal(1), Nil())), Cons(Rule(NonTerminal(0), Cons(NonTerminal(0), Cons(Terminal(1), Nil()))), Nil()))) =>
-      "<b>Start:</b> S0<br><pre>S0 -> t1<br>S0 -> S0 t1</pte>"
   
   /* The initial body of this function is the solution of render3 */
   def render5PlainTextRules(s: Grammar): String = {