diff --git a/src/main/scala/leon/purescala/DefinitionTransformer.scala b/src/main/scala/leon/purescala/DefinitionTransformer.scala
index 2588ed8fe33419c1becb753506362c0ca663388f..6dfea1dbe2cf359b0839a65739149a57aab406e9 100644
--- a/src/main/scala/leon/purescala/DefinitionTransformer.scala
+++ b/src/main/scala/leon/purescala/DefinitionTransformer.scala
@@ -45,11 +45,6 @@ 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/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index e69050bf6c0b89388f9834e9890262e0a9817a6d..98d819eb2dd9031585ba1fb249142cb8f6629773 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -180,6 +180,9 @@ object FunctionClosure extends TransformationPhase {
       case _ => None
     }(instBody)
 
+    //HACK to make sure substitution happened even in nested fundef
+    newFd.fullBody = replaceFromIDs(freeMap.map(p => (p._1, p._2.toVariable)), newFd.fullBody)
+
     FunSubst(newFd, freeMap, tparamsMap.map{ case (from, to) => from.tp -> to})
   }
 
diff --git a/src/main/scala/leon/purescala/TreeTransformer.scala b/src/main/scala/leon/purescala/TreeTransformer.scala
index d74da4f8fb2781e9f4fbe1b0c3481c0292a33125..a1f6e2ad68859fcb2d13e1444e69aa90f4061559 100644
--- a/src/main/scala/leon/purescala/TreeTransformer.scala
+++ b/src/main/scala/leon/purescala/TreeTransformer.scala
@@ -38,6 +38,10 @@ trait TreeTransformer {
     case LetVar(a, expr, body) =>
       val newA = transform(a)
       LetVar(newA, transform(expr), transform(body)(bindings + (a -> newA))).copiedFrom(e)
+    case LetDef(fds, body) =>
+      val rFds = fds map transform
+      val rBody = transform(body)
+      LetDef(rFds, rBody).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/test/resources/regression/verification/purescala/valid/Nested18.scala b/src/test/resources/regression/verification/purescala/valid/Nested18.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a35c2f4b9722ee9e663637d9d26f40570623ed94
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Nested18.scala
@@ -0,0 +1,15 @@
+object Nested18 {
+
+  def test(a: BigInt): BigInt = {
+    require(a > 0)
+    def f(b: BigInt): BigInt = {
+      def g(c: BigInt): BigInt = {
+        require(a > 0)
+        c
+      }
+      g(b)
+    }
+    f(12)
+  }
+
+}
diff --git a/src/test/scala/leon/unit/purescala/FunctionClosureSuite.scala b/src/test/scala/leon/unit/purescala/FunctionClosureSuite.scala
index faef381959bcb4e219a9c1fe603a485791627613..2019c04525eaa05f9030f3a7068b19a149105d2c 100644
--- a/src/test/scala/leon/unit/purescala/FunctionClosureSuite.scala
+++ b/src/test/scala/leon/unit/purescala/FunctionClosureSuite.scala
@@ -97,6 +97,38 @@ class FunctionClosureSuite extends FunSuite with helpers.ExpressionsDSL {
         fail("Unexpected fun def: " + cfd)
       }
     })
+
+
+    val deeplyNested2 = new FunDef(FreshIdentifier("deeplyNested"), Seq(), Seq(ValDef(z.id)), IntegerType)
+    deeplyNested2.body = Some(Require(GreaterEquals(x, bi(0)), z))
+
+    val nested2 = new FunDef(FreshIdentifier("nested"), Seq(), Seq(ValDef(y.id)), IntegerType)
+    nested2.body = Some(LetDef(Seq(deeplyNested2), FunctionInvocation(deeplyNested2.typed, Seq(y))))
+
+    val fd2 = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(x.id)), IntegerType)
+    fd2.body = Some(Require(GreaterEquals(x, bi(0)),
+                    LetDef(Seq(nested2), FunctionInvocation(nested2.typed, Seq(x)))))
+
+    val cfds2 = FunctionClosure.close(fd2)
+    assert(cfds2.size === 3)
+
+    cfds2.foreach(cfd => {
+      if(cfd.id.name == "f") {
+        assert(cfd.returnType === fd2.returnType)
+        assert(cfd.params.size === fd2.params.size)
+        assert(freeVars(cfd).isEmpty)
+      } else if(cfd.id.name == "nested") {
+        assert(cfd.returnType === nested2.returnType)
+        assert(cfd.params.size === 2)
+        assert(freeVars(cfd).isEmpty)
+      } else if(cfd.id.name == "deeplyNested") {
+        assert(cfd.returnType === deeplyNested2.returnType)
+        assert(cfd.params.size === 2)
+        assert(freeVars(cfd).isEmpty)
+      } else {
+        fail("Unexpected fun def: " + cfd)
+      }
+    })
   }
 
   private def freeVars(fd: FunDef): Set[Identifier] = variablesOf(fd.fullBody) -- fd.paramIds