diff --git a/src/main/scala/leon/purescala/DefinitionTransformer.scala b/src/main/scala/leon/purescala/DefinitionTransformer.scala
index d0008e5b6af0d04f27cae0157da1d94e44b7dd48..abe08fa34fd66465bbcf2c2ba7c114d5075c592c 100644
--- a/src/main/scala/leon/purescala/DefinitionTransformer.scala
+++ b/src/main/scala/leon/purescala/DefinitionTransformer.scala
@@ -34,6 +34,12 @@ class DefinitionTransformer(
           idMap += id -> nid
           nid
       })
+
+    case LetDef(fds, body) =>
+      val rFds = fds map transform
+      val rBody = transform(body)
+      LetDef(rFds, rBody).copiedFrom(e)
+      
     case _ => super.transform(e)
   }
 
diff --git a/src/main/scala/leon/purescala/TreeTransformer.scala b/src/main/scala/leon/purescala/TreeTransformer.scala
index 77a5659f1dbb8d49d7b81983656e33eaaa128a9c..d74da4f8fb2781e9f4fbe1b0c3481c0292a33125 100644
--- a/src/main/scala/leon/purescala/TreeTransformer.scala
+++ b/src/main/scala/leon/purescala/TreeTransformer.scala
@@ -6,6 +6,7 @@ package purescala
 import Common._
 import Definitions._
 import Expressions._
+import xlang.Expressions._
 import Extractors._
 import Types._
 
@@ -34,6 +35,9 @@ trait TreeTransformer {
     case Let(a, expr, body) =>
       val newA = transform(a)
       Let(newA, transform(expr), transform(body)(bindings + (a -> newA))).copiedFrom(e)
+    case LetVar(a, expr, body) =>
+      val newA = transform(a)
+      LetVar(newA, transform(expr), transform(body)(bindings + (a -> newA))).copiedFrom(e)
     case CaseClass(cct, args) =>
       CaseClass(transform(cct).asInstanceOf[CaseClassType], args map transform).copiedFrom(e)
     case CaseClassSelector(cct, caseClass, selector) =>
diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index b721a94726a956c71d4d84364105ab5fd111fbb3..063694addccde2f2e4e4df3c399109937f30312d 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -84,6 +84,7 @@ object AntiAliasingPhase extends TransformationPhase {
     } {
       updatedFunctions += (fd -> updateFunDef(fd, effects)(ctx))
     }
+    //println(updatedFunctions.filter(p => p._1.id != p._2.id).mkString("\n"))
 
     for {
       fd <- fds
diff --git a/src/test/resources/regression/verification/xlang/valid/ExpressionOrder1.scala b/src/test/resources/regression/verification/xlang/valid/ExpressionOrder1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c34d2057e3c945283cf8548393c1ad97e4c11886
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ExpressionOrder1.scala
@@ -0,0 +1,19 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+import leon.lang._
+
+object NestedFunState8 {
+
+  def test1 = {
+    var x = 0
+
+    def bar(y: Int) = {
+      def fun(z: Int) = 1 * x * (y + z)
+
+      fun(3)
+    }
+
+    bar(2) == 0
+  }.holds
+
+}