diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
index 45d4fe43c..610cc514e 100644
--- a/src/main/scala/rules/Evaluator.scala
+++ b/src/main/scala/rules/Evaluator.scala
@@ -291,9 +291,9 @@ object evaluator extends EvaluationRules {
 
       case ast.Let(x, e0, e1) =>
         eval(s, e0, pve, v)((s1, t0, v1) => {
-          val t = v1.decider.fresh(v1.symbolConverter.toSort(x.typ))
+          val t = v1.decider.appliedFresh("letvar", v1.symbolConverter.toSort(x.typ), s1.relevantQuantifiedVariables)
           v1.decider.assume(t === t0)
-          val newFuncRec = s1.functionRecorder.recordFreshSnapshot(t)
+          val newFuncRec = s1.functionRecorder.recordFreshSnapshot(t.applicable.asInstanceOf[Function])
           eval(s1.copy(g = s1.g + (x.localVar, t0), functionRecorder = newFuncRec), e1, pve, v1)(Q)
         })