diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 0014d38766e84b5a75b77859da7bc0974c60d358..d935a7f05ae7ba26efe666e37f72becdcca89195 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -53,11 +53,10 @@ class PrettyPrinter(opts: PrinterOptions,
 
   def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
 
-    if (requiresBraces(tree, ctx.parent)) {
-      val ctx1: PrinterContext = ctx.copy(parents = Nil)
+    if (requiresBraces(tree, ctx.parent) && !ctx.parent.contains(tree)) {
       p"""|{
           |  $tree
-          |}"""(ctx1)
+          |}"""
       return
     }
 
@@ -213,14 +212,14 @@ class PrettyPrinter(opts: PrinterOptions,
           p"($presentArgs)"
         }
 
-      case FunctionInvocation(tfd, args) =>
-        p"${tfd.id}"
+      case FunctionInvocation(TypedFunDef(fd, tps), args) =>
+        printWithPath(fd)
 
-        if (tfd.tps.nonEmpty) {
-          p"[${tfd.tps}]"
+        if (tps.nonEmpty) {
+          p"[$tps]"
         }
 
-        if (tfd.fd.isRealFunction) { 
+        if (fd.isRealFunction) {
           // The non-present arguments are synthetic function invocations
           val presentArgs = args filter {
             case MethodInvocation(_, _, tfd, _) if tfd.fd.isSynthetic => false
@@ -377,12 +376,17 @@ class PrettyPrinter(opts: PrinterOptions,
         ob.foreach { b => p"$b @ " }
 
         // @mk: I admit this is pretty ugly
-        val id = for {
+        (for {
           p <- opgm
           mod <- p.modules.find( _.definedFunctions contains tfd.fd )
-        } yield mod.id
-
-        p"${id.getOrElse("<unknown object>")}(${nary(subps)})"
+        } yield mod) match {
+          case Some(obj) =>
+            printWithPath(obj)
+          case None =>
+            p"<unkown object>"
+        }
+        
+        p"(${nary(subps)})"
 
       case LiteralPattern(ob, lit) =>
         ob foreach { b => p"$b @ " }
diff --git a/src/main/scala/leon/purescala/PrinterHelpers.scala b/src/main/scala/leon/purescala/PrinterHelpers.scala
index 46ca1ae30ca1a814127206cbf0c640410de16101..c2894173f5d3745afcd8114a330321ad73b6e526 100644
--- a/src/main/scala/leon/purescala/PrinterHelpers.scala
+++ b/src/main/scala/leon/purescala/PrinterHelpers.scala
@@ -54,7 +54,8 @@ object PrinterHelpers {
               nary(ts).print(nctx)
 
             case t: Tree =>
-              val parents = if (nctx.current == t) {
+              // Don't add same tree twice in parents
+              val parents = if (nctx.parents.headOption contains nctx.current) {
                 nctx.parents
               } else {
                 nctx.current :: nctx.parents