diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 727e0d94b22694a5722a76fc867dad82e5408554..778c0679c85556ffb547aef153bdde232839d9da 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -33,10 +33,8 @@ object ExprOps {
    */
   def foldRight[T](f: (Expr, Seq[T]) => T)(e: Expr): T = {
     val rec = foldRight(f) _
-
     val Operator(es, _) = e
     f(e, es.view.map(rec))
-
   }
 
   /**
@@ -53,8 +51,8 @@ object ExprOps {
    */
   def preTraversal(f: Expr => Unit)(e: Expr): Unit = {
     val rec = preTraversal(f) _
-    f(e)
     val Operator(es, _) = e
+    f(e)
     es.foreach(rec)
   }
 
@@ -189,29 +187,7 @@ object ExprOps {
     }
     v2
   }
-
-  
-  
   
-  ///*
-  // * Turn a total function returning Option[A] into a partial function
-  // * returning A.
-  // * Optimize for isDefinedAt -> apply access pattern
-  // */
-  //def unlift[A, B](f: A => Option[B]): PartialFunction[A,B] = new PartialFunction[A, B] {
-  //  var last: Option[(A, Option[B])] = None
-
-  //  def apply(a: A) = last match {
-  //    case Some((a2, res)) if a2 == a => res.get
-  //    case _ => f(a).get
-  //  }
-
-  //  def isDefinedAt(a: A) = {
-  //    val res = f(a)
-  //    last = Some((a, res))
-  //    res.isDefined
-  //  }
-  //}
 
   /**
    * Auxiliary API
@@ -930,6 +906,7 @@ object ExprOps {
     case act @ AbstractClassType(acd, tpe) =>
       val children = acd.knownChildren
 
+      // FIXME: What if deep hierarchies? What if Cons[Option[List[A]]]?
       def isRecursive(ccd: CaseClassDef): Boolean = {
         act.fieldsTypes.exists{
           case AbstractClassType(fieldAcd, _) => acd == fieldAcd
@@ -983,7 +960,7 @@ object ExprOps {
       case _ => None
     }
 
-    fixpoint(postMap(transform))(expr)
+    postMap(transform, applyRec = true)(expr)
   }
 
   def genericTransform[C](pre:  (Expr, C) => (Expr, C),
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 32de020857ab8edccd9c3d2e4d1a00dc4fb08910..5e5d3407d4faf8bdd4e978d67c59931104eaaf11 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -175,17 +175,17 @@ class PrettyPrinter(opts: PrinterOptions,
       case BVUMinus(expr)       => p"-$expr"
       case Equals(l,r)          => optP { p"$l == $r" }
       case IntLiteral(v)        => p"$v"
-      case InfiniteIntegerLiteral(v)        => p"$v"
+      case InfiniteIntegerLiteral(v) => p"$v"
       case CharLiteral(v)       => p"$v"
       case BooleanLiteral(v)    => p"$v"
       case UnitLiteral()        => p"()"
       case GenericValue(tp, id) => p"$tp#$id"
       case Tuple(exprs)         => p"($exprs)"
       case TupleSelect(t, i)    => p"$t._$i"
-      case NoTree(tpe)          => p"???($tpe)"
+      case NoTree(tpe)          => p"???[$tpe]"
       case Choose(pred)         => p"choose($pred)"
-      case e @ Error(tpe, err)       => p"""error[$tpe]("$err")"""
-      case IsInstanceOf(cct, e)         =>
+      case e @ Error(tpe, err)  => p"""error[$tpe]("$err")"""
+      case IsInstanceOf(cct, e) =>
         if (cct.classDef.isCaseObject) {
           p"($e == $cct)"
         } else {