diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 8249e0d9e..854684591 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -373,7 +373,7 @@ public abstract class VCExprNAry : VCExpr
   {
     public override string ToString()
     {
-      return $"${Op}(${String.Join(", ", Arguments)})";
+      return $"{Op}({String.Join(", ", Arguments)})";
     }
 
     [Pure]
@@ -1765,6 +1765,11 @@ public override Result Accept<Result, Arg>(
       //Contract.Requires(expr != null);
       return visitor.VisitBoogieFunctionOp(expr, arg);
     }
+
+    public override string ToString()
+    {
+      return Func.Name;
+    }
   }
 
   /////////////////////////////////////////////////////////////////////////////////
diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index 47ad03bfc..d125b696b 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -1112,29 +1112,6 @@ public SubstitutingVCExprVisitor(VCExpressionGenerator gen)
       Contract.Requires(gen != null);
     }
 
-    // when descending across a binder, we have to check that no collisions
-    // or variable capture can occur. if this might happen, we replace the
-    // term and type variables bound by the binder with fresh variables
-    private bool CollisionPossible(IEnumerable<TypeVariable /*!*/> /*!*/ typeParams,
-      IEnumerable<VCExprVar /*!*/> /*!*/ boundVars, VCExprSubstitution /*!*/ substitution)
-    {
-      Contract.Requires(Cce.NonNullElements(typeParams));
-      Contract.Requires(Cce.NonNullElements(boundVars));
-      Contract.Requires(substitution != null);
-      // variables can be shadowed by a binder
-      if (typeParams.Any(var => substitution.ContainsKey(var)) ||
-          boundVars.Any(var => substitution.ContainsKey(var)))
-      {
-        return true;
-      }
-      // compute the codomain of the substitution
-      FreeVariableCollector coll = substitution.Codomains;
-      Contract.Assert(coll != null);
-      // variables could be captured when applying the substitution
-      return typeParams.Any(var => coll.FreeTypeVars.Contains(var)) ||
-             boundVars.Any(var => coll.FreeTermVars.Contains(var));
-    }
-
     // can be overwritten if names of bound variables are to be changed
     protected virtual string ChooseNewVariableName(string oldName)
     {
@@ -1184,51 +1161,18 @@ protected virtual string ChooseNewVariableName(string oldName)
       Contract.Requires(substitution != null);
       Contract.Ensures(Contract.Result<VCExpr>() != null);
 
-      // the default is to refresh bound variables only if necessary
-      // because of collisions
-      return Visit(node, substitution, false);
-    }
-
-    public VCExpr /*!*/ Visit(VCExprQuantifier /*!*/ node, VCExprSubstitution /*!*/ substitution,
-      bool refreshBoundVariables)
-    {
-      Contract.Requires(node != null);
-      Contract.Requires(substitution != null);
-      Contract.Ensures(Contract.Result<VCExpr>() != null);
-
       substitution.PushScope();
       try
       {
         List<TypeVariable /*!*/> /*!*/
           typeParams = node.TypeParameters;
         Contract.Assert(Cce.NonNullElements(typeParams));
-        bool refreshAllVariables = refreshBoundVariables ||
-                                   CollisionPossible(node.TypeParameters, node.BoundVars, substitution);
-        if (refreshAllVariables)
-        {
-          // we introduce fresh type variables to ensure that none gets captured
-          typeParams = new List<TypeVariable /*!*/>();
-          foreach (TypeVariable /*!*/ var in node.TypeParameters)
-          {
-            Contract.Assert(var != null);
-            TypeVariable /*!*/
-              freshVar =
-                new TypeVariable(Token.NoToken, ChooseNewVariableName(var.Name));
-            Contract.Assert(freshVar != null);
-            typeParams.Add(freshVar);
-            substitution[var] = freshVar;
-            // this might overwrite other elements of the substitution, deliberately
-          }
-        }
-
         List<VCExprVar /*!*/> /*!*/
           boundVars = node.BoundVars;
         Contract.Assert(Cce.NonNullElements(boundVars));
-        if (refreshAllVariables || !substitution.TypeSubstIsEmpty)
+        if (!substitution.TypeSubstIsEmpty)
         {
-          // collisions are possible, or we also substitute type variables. in this case
-          // the bound term variables have to be replaced with fresh variables with the
-          // right types
+          // replace each bound term variable with a fresh variable of correct type
           boundVars = new List<VCExprVar /*!*/>();
           IDictionary<TypeVariable /*!*/, Type /*!*/> /*!*/
             typeSubst = substitution.ToTypeSubst;
@@ -1243,7 +1187,6 @@ protected virtual string ChooseNewVariableName(string oldName)
             Contract.Assert(freshVar != null);
             boundVars.Add(freshVar);
             substitution[var] = freshVar;
-            // this might overwrite other elements of the substitution, deliberately
           }
         }
 
@@ -1283,16 +1226,6 @@ public override VCExpr Visit(VCExprVar node, VCExprSubstitution substitution)
     }
 
     public override VCExpr Visit(VCExprLet node, VCExprSubstitution substitution)
-    {
-      Contract.Requires(substitution != null);
-      Contract.Requires(node != null);
-      Contract.Ensures(Contract.Result<VCExpr>() != null);
-      // the default is to refresh bound variables only if necessary
-      // because of collisions
-      return Visit(node, substitution, false);
-    }
-
-    public VCExpr Visit(VCExprLet node, VCExprSubstitution substitution, bool refreshBoundVariables)
     {
       Contract.Requires(substitution != null);
       Contract.Requires(node != null);
@@ -1301,19 +1234,12 @@ public VCExpr Visit(VCExprLet node, VCExprSubstitution substitution, bool refres
       substitution.PushScope();
       try
       {
-        bool refreshAllVariables =
-          refreshBoundVariables ||
-          !substitution.TypeSubstIsEmpty ||
-          CollisionPossible(new List<TypeVariable /*!*/>(), node.BoundVars, substitution);
-
         List<VCExprVar /*!*/> /*!*/
           newBoundVars = node.BoundVars;
         Contract.Assert(Cce.NonNullElements(newBoundVars));
-        if (refreshAllVariables)
+        if (!substitution.TypeSubstIsEmpty)
         {
-          // collisions are possible, or we also substitute type variables. in this case
-          // the bound term variables have to be replaced with fresh variables with the
-          // right types
+          // replace each bound term variable with a fresh variable of correct type
           newBoundVars = new List<VCExprVar /*!*/>();
           IDictionary<TypeVariable /*!*/, Type /*!*/> /*!*/
             typeSubst = substitution.ToTypeSubst;
@@ -1328,7 +1254,6 @@ public VCExpr Visit(VCExprLet node, VCExprSubstitution substitution, bool refres
             Contract.Assert(freshVar != null);
             newBoundVars.Add(freshVar);
             substitution[var] = freshVar;
-            // this might overwrite other elements of the substitution, deliberately
           }
         }