diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index eb5191189a62f1c78fdb503949d2b0617218ff31..f723b2d7f8c3f32818602cd5c1583605b8690a5e 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -394,13 +394,10 @@ trait CodeExtraction extends Extractors {
         varSubsts.remove(vs)
         Let(newID, valTree, restTree)
       }
-      case dd @ ExLocalFunctionDef(n, p, t, b, rest) => {
+      case dd @ ExLocalFunctionDef(sy,n, p, t, b, rest) => {
         val funDef = extractFunSig(n, p, t).setPosInfo(dd.pos.line, dd.pos.column)
         val funDefWithBody = extractFunDef(funDef, b)
-        println("got let def: " + funDefWithBody)
-        println(funDef)
-        defsToDefs += (dd.symbol -> funDefWithBody)
-        println(defsToDefs)
+        defsToDefs += (sy -> funDefWithBody)
         val letRest = rec(rest)
         defsToDefs.remove(dd.symbol)
         val res = LetDef(funDefWithBody, letRest)
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index 8b55cf10d5ddf48a5a4aa4ef4a7100668dbe8d62..26096444c5328ae67332cc26c0d0c304a687929b 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -152,12 +152,12 @@ trait Extractors {
     }
 
     object ExLocalFunctionDef {
-      def unapply(tree: Block): Option[(String,Seq[ValDef],Tree,Tree,Tree)] = tree match {
+      def unapply(tree: Block): Option[(Symbol,String,Seq[ValDef],Tree,Tree,Tree)] = tree match {
         case Block((dd @ DefDef(_, name, tparams, vparamss, tpt, rhs)) :: rest, expr) if(tparams.isEmpty && vparamss.size == 1 && name != nme.CONSTRUCTOR) => {
           if(rest.isEmpty)
-            Some((name.toString, vparamss(0), tpt, rhs, expr))
+            Some((dd.symbol,name.toString, vparamss(0), tpt, rhs, expr))
           else
-            Some((name.toString, vparamss(0), tpt, rhs, Block(rest, expr)))
+            Some((dd.symbol,name.toString, vparamss(0), tpt, rhs, Block(rest, expr)))
         } 
         case _ => None
       }
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 98cbee8852e8b6d0ca3bb442d30890f98ad1cb94..b16515c4a14d47b9eccfae86eba42e6a5ff94424 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -74,6 +74,8 @@ object PrettyPrinter {
     case LetDef(fd,e) => {
       sb.append("{")
       pp(fd, sb, lvl)
+      sb.append("\n")
+      ind(sb, lvl)
       pp(e, sb, lvl)
       sb.append("}")
       sb