diff --git a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
index 09fc6b67870..55e0f65aebe 100644
--- a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
+++ b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
@@ -457,16 +457,23 @@ let rec (free_vars_b :
       fun binder ->
         match binder.FStar_Parser_AST.b with
         | FStar_Parser_AST.Variable x ->
-            let uu___ = FStar_Syntax_DsEnv.push_bv env x in
-            (match uu___ with | (env1, uu___1) -> (env1, []))
+            if tvars_only
+            then (env, [])
+            else
+              (let uu___1 = FStar_Syntax_DsEnv.push_bv env x in
+               match uu___1 with | (env1, uu___2) -> (env1, []))
         | FStar_Parser_AST.TVariable x ->
             let uu___ = FStar_Syntax_DsEnv.push_bv env x in
             (match uu___ with | (env1, uu___1) -> (env1, [x]))
         | FStar_Parser_AST.Annotated (x, term) ->
-            let uu___ = FStar_Syntax_DsEnv.push_bv env x in
-            (match uu___ with
-             | (env', uu___1) ->
-                 let uu___2 = free_vars tvars_only env term in (env', uu___2))
+            if tvars_only
+            then let uu___ = free_vars tvars_only env term in (env, uu___)
+            else
+              (let uu___1 = FStar_Syntax_DsEnv.push_bv env x in
+               match uu___1 with
+               | (env', uu___2) ->
+                   let uu___3 = free_vars tvars_only env term in
+                   (env', uu___3))
         | FStar_Parser_AST.TAnnotated (id, term) ->
             let uu___ = FStar_Syntax_DsEnv.push_bv env id in
             (match uu___ with
diff --git a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
index 62f90dcdc71..278cb031bf2 100644
--- a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
+++ b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
@@ -289,14 +289,22 @@ let sort_ftv ftv =
 let rec free_vars_b tvars_only env binder : (Env.env & list ident) =
   match binder.b with
   | Variable x ->
-    let env, _ = Env.push_bv env x in
-    env, []
+    if tvars_only
+    then env, [] //tvars can't clash with vars
+    else (
+      let env, _ = Env.push_bv env x in
+      env, []
+    )
   | TVariable x ->
     let env, _ = Env.push_bv env x in
     env, [x]
   | Annotated(x, term) ->
-    let env', _ = Env.push_bv env x in
-    env', free_vars tvars_only env term
+    if tvars_only  //tvars can't clash with vars
+    then env, free_vars tvars_only env term
+    else (
+      let env', _ = Env.push_bv env x in
+      env', free_vars tvars_only env term
+    )
   | TAnnotated(id, term) ->
     let env', _ = Env.push_bv env id in
     env', free_vars tvars_only env term