diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index f0b2a975b1517b2f9fd31422d3e9a911f9489d98..c188491b408216e82b0d2a727f93958bb66d21ed 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -306,6 +306,13 @@ object Constructors {
   }
 
   /** $encodingof simplified `fn(realArgs)` (function application).
+    * Transforms
+    * {{{ ((x: A, y: B) => g(x, y))(c, d) }}}
+    * into
+    * {{{val x0 = c
+    * val y0 = d
+    * g(x0, y0)}}}
+    * and further simplifies it.
     * @see [[purescala.Expressions.Lambda Lambda]]
     * @see [[purescala.Expressions.Application Application]]
     */
diff --git a/src/main/scala/leon/purescala/ScopeSimplifier.scala b/src/main/scala/leon/purescala/ScopeSimplifier.scala
index 7bae40c5bb4df6c6b54c476fc6c406e97f89ec9a..d2b4686b6358bd5eb306b54ebf27a0599adb6d3f 100644
--- a/src/main/scala/leon/purescala/ScopeSimplifier.scala
+++ b/src/main/scala/leon/purescala/ScopeSimplifier.scala
@@ -3,6 +3,7 @@
 package leon
 package purescala
 
+import collection.mutable.ListBuffer
 import Common._
 import Definitions._
 import Expressions._
@@ -10,11 +11,15 @@ import Extractors._
 
 class ScopeSimplifier extends Transformer {
   case class Scope(inScope: Set[Identifier] = Set(), oldToNew: Map[Identifier, Identifier] = Map(), funDefs: Map[FunDef, FunDef] = Map()) {
-
+    
     def register(oldNew: (Identifier, Identifier)): Scope = {
       val newId = oldNew._2
       copy(inScope = inScope + newId, oldToNew = oldToNew + oldNew)
     }
+    
+    def register(oldNews: Seq[(Identifier, Identifier)]): Scope = {
+      (this /: oldNews){ case (oldScope, oldNew) => oldScope.register(oldNew) }
+    }
 
     def registerFunDef(oldNew: (FunDef, FunDef)): Scope = {
       copy(funDefs = funDefs + oldNew)
@@ -37,27 +42,28 @@ class ScopeSimplifier extends Transformer {
     case LetDef(fds, body: Expr) =>
       var newScope: Scope = scope
       // First register all functions
-      val fds_newIds = for(fd <- fds) yield {
+      val fds_newIds = for(fd <- fds) yield { // Problem if some functions use the same ID for a ValDef
         val newId    = genId(fd.id, scope)
         newScope = newScope.register(fd.id -> newId)
         (fd, newId)
       }
       
       val fds_mapping = for((fd, newId) <- fds_newIds) yield {
+        val localScopeToRegister = ListBuffer[(Identifier, Identifier)]() // We record the mapping of these variables only for the function.
         val newArgs = for(ValDef(id, tpe) <- fd.params) yield {
-          val newArg = genId(id, newScope)
-          newScope = newScope.register(id -> newArg)
+          val newArg = genId(id, newScope.register(localScopeToRegister))
+          localScopeToRegister += (id -> newArg) // This should happen only inside the function.
           ValDef(newArg, tpe)
         }
   
         val newFd = fd.duplicate(id = newId, params = newArgs)
   
         newScope = newScope.registerFunDef(fd -> newFd)
-        (newFd, fd)
+        (newFd, localScopeToRegister, fd)
       }
       
-      for((newFd, fd) <- fds_mapping) {
-        newFd.fullBody = rec(fd.fullBody, newScope)
+      for((newFd, localScopeToRegister, fd) <- fds_mapping) {
+        newFd.fullBody = rec(fd.fullBody, newScope.register(localScopeToRegister))
       }
       LetDef(fds_mapping.map(_._1), rec(body, newScope))
    
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index e8a78e1434e71e8980c15e3da94049ead450d9f8..b3239492211950f692e7c1a956e2d18e3619274c 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -476,8 +476,7 @@ case object StringRender extends Rule("StringRender") {
               gatherInputs(ctx, q, result +=
                 mergeResults(Stream((input, Nil),
                         (functionInvocation(
-                            hctx.program.library.escape.get,
-                            input::ctx.provided_functions.toList.map(Variable)): Expr, Nil))))
+                            hctx.program.library.escape.get, List(input)): Expr, Nil))))
             case BooleanType =>
               val (bTemplate, vs) = booleanTemplate(input).instantiateWithVars
               gatherInputs(ctx, q, result += mergeResults(Stream((BooleanToString(input), Nil), (bTemplate, vs))))