diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index dde462e0cc81518779dc5bb2bfbf893e7489540f..43544f617e097883879a134828a580386729dbbd 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -12,7 +12,6 @@ import leon.purescala.PrinterHelpers._
 import leon.purescala.ExprOps.{isListLiteral, simplestValue}
 import leon.purescala.Expressions._
 import leon.purescala.Types._
-import leon.synthesis.Witnesses._
 
 case class PrinterContext(
   current: Tree,
@@ -157,7 +156,7 @@ class PrettyPrinter(opts: PrinterOptions,
         }
 
       case And(exprs)           => optP { p"${nary(exprs, " && ")}" }
-      case Or(exprs)            => optP { p"${nary(exprs, "| || ")}" }
+      case Or(exprs)            => optP { p"${nary(exprs, " || ")}" }
       case Not(Equals(l, r))    => optP { p"$l \u2260 $r" }
       case Implies(l,r)         => optP { p"$l ==> $r" }
       case UMinus(expr)         => p"-$expr"
@@ -332,12 +331,6 @@ class PrettyPrinter(opts: PrinterOptions,
               |} else $ie"""
         }
 
-      case Terminating(tfd, args) =>
-        p"↓ ${tfd.id}($args)"
-
-      case Guide(e) =>
-        p"⊙ {$e}"
-
       case IfExpr(c, t, e) =>
         optP {
           p"""|if ($c) {
@@ -348,20 +341,14 @@ class PrettyPrinter(opts: PrinterOptions,
         }
 
       case LetPattern(p,s,rhs) => 
-        rhs match { 
-          case _:LetDef | _ : Let | LetPattern(_,_,_) =>
-            optP {
-              p"""|val $p = {
-                  |  $s
-                  |}
-                  |$rhs"""
-            }
-
-          case _ => 
-            optP {
-              p"""|val $p = $s
-                  |$rhs"""
-            }
+        if (isSimpleExpr(s)) {
+          p"""|val $p = $s
+              |$rhs"""
+        } else {
+          p"""|val $p = {
+              |  $s
+              |}
+              |$rhs"""
         }
 
       case MatchExpr(s, csc) =>
diff --git a/src/main/scala/leon/purescala/PrinterHelpers.scala b/src/main/scala/leon/purescala/PrinterHelpers.scala
index e0aed391cfb46c28fa2d4295995c2c2b1069ae20..b0fb6e7226a349ec138e09be4f88c743ebfc5fea 100644
--- a/src/main/scala/leon/purescala/PrinterHelpers.scala
+++ b/src/main/scala/leon/purescala/PrinterHelpers.scala
@@ -5,7 +5,6 @@ package purescala
 
 import purescala.Common._
 import purescala.Types._
-import purescala.Definitions._
 
 object PrinterHelpers {
   implicit class Printable(val f: PrinterContext => Any) extends AnyVal {
@@ -42,7 +41,7 @@ object PrinterHelpers {
         // Make sure new lines are also indented
         sb.append(s.replaceAll("\n", "\n"+("  "*ctx.lvl)))
 
-        var nctx = ctx.copy(lvl = ctx.lvl + extraInd)
+        val nctx = ctx.copy(lvl = ctx.lvl + extraInd)
 
         if (expressions.hasNext) {
           val e = expressions.next
diff --git a/src/main/scala/leon/synthesis/Witnesses.scala b/src/main/scala/leon/synthesis/Witnesses.scala
index 1213766ec5aad957e8af5f5f9c6abbccb33d1c1c..0325c4a8a10bbe460050a63ff0c65d326fd9662e 100644
--- a/src/main/scala/leon/synthesis/Witnesses.scala
+++ b/src/main/scala/leon/synthesis/Witnesses.scala
@@ -7,20 +7,28 @@ import Types._
 import Definitions.TypedFunDef
 import Extractors._
 import Expressions.Expr
-
+import PrinterHelpers._
 
 object Witnesses {
   
-  class Witness extends Expr {
+  abstract class Witness extends Expr with Extractable with PrettyPrintable {
     val getType = BooleanType
   }
   
-  case class Guide(e : Expr) extends Witness with Extractable {
+  case class Guide(e : Expr) extends Witness {
     def extract: Option[(Seq[Expr], Seq[Expr] => Expr)] = Some((Seq(e), (es: Seq[Expr]) => Guide(es.head)))
+
+    override def printWith(implicit pctx: PrinterContext): Unit = {
+      p"⊙ {$e}"
+    }
   }
   
-  case class Terminating(tfd: TypedFunDef, args: Seq[Expr]) extends Witness with Extractable {
+  case class Terminating(tfd: TypedFunDef, args: Seq[Expr]) extends Witness {
     def extract: Option[(Seq[Expr], Seq[Expr] => Expr)] = Some((args, Terminating(tfd, _)))
+
+    override def printWith(implicit pctx: PrinterContext): Unit = {
+      p"↓ ${tfd.id}($args)"
+    }
   }
   
 }