diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 73fcb4849f1774d237f9dcf5369671af4abf3573..1cee46865717b0e214e66ff41fac0c07039031fa 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -341,7 +341,7 @@ object ExprOps {
 
   /** Returns the set of free variables in an expression */
   def variablesOf(expr: Expr): Set[Identifier] = {
-    import leon.xlang.Expressions.LetVar
+    import leon.xlang.Expressions._
     fold[Set[Identifier]] {
       case (e, subs) =>
         val subvs = subs.flatten.toSet
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 513720ff411d942972c7a15f0692d218a406576b..76a75fdf263248e7045ebeb959fb65750b4767ad 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -76,10 +76,6 @@ object Expressions {
     val getType = tpe
   }
 
-  case class Old(id: Identifier) extends Expr with Terminal {
-    val getType = id.getType
-  }
-
   /** Precondition of an [[Expressions.Expr]]. Corresponds to the Leon keyword *require*
     *
     * @param pred The precondition formula inside ``require(...)``
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 039bef507339294874ad59e7e38dfe335b8f6a2f..44d454a9c0a4f1127ed0533f872c66f1ec6bc067 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -81,15 +81,12 @@ class PrettyPrinter(opts: PrinterOptions,
         }
         p"$name"
 
-      case Old(id) =>
-        p"old($id)"
-
       case Variable(id) =>
         p"$id"
 
       case Let(b,d,e) =>
-          p"""|val $b = $d
-              |$e"""
+        p"""|val $b = $d
+            |$e"""
 
       case LetDef(a::q,body) =>
         p"""|$a
diff --git a/src/main/scala/leon/xlang/Expressions.scala b/src/main/scala/leon/xlang/Expressions.scala
index d627e0d284f4933cd6ed7ecefbe7dd13f4e658f8..98214ee640bd95227c0b759113ab74d2c9555d94 100644
--- a/src/main/scala/leon/xlang/Expressions.scala
+++ b/src/main/scala/leon/xlang/Expressions.scala
@@ -15,6 +15,14 @@ object Expressions {
 
   trait XLangExpr extends Expr
 
+  case class Old(id: Identifier) extends XLangExpr with Terminal with PrettyPrintable {
+    val getType = id.getType
+
+    def printWith(implicit pctx: PrinterContext): Unit = {
+      p"old($id)"
+    }
+  }
+
   case class Block(exprs: Seq[Expr], last: Expr) extends XLangExpr with Extractable with PrettyPrintable {
     def extract: Option[(Seq[Expr], (Seq[Expr])=>Expr)] = {
       Some((exprs :+ last, exprs => Block(exprs.init, exprs.last)))