diff --git a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
index 20450208b93..09fc6b67870 100644
--- a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
+++ b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
@@ -515,11 +515,13 @@ and (free_vars :
             else
               (let ids = FStar_Ident.ids_of_lid x in
                match ids with
-               | x1::[] ->
-                   let uu___2 = FStar_Syntax_DsEnv.try_lookup_id env x1 in
-                   (match uu___2 with
-                    | FStar_Pervasives_Native.None -> [x1]
-                    | uu___3 -> [])
+               | id::[] ->
+                   let uu___2 =
+                     (let uu___3 = FStar_Syntax_DsEnv.try_lookup_id env id in
+                      FStar_Pervasives_Native.uu___is_None uu___3) &&
+                       (let uu___3 = FStar_Syntax_DsEnv.try_lookup_lid env x in
+                        FStar_Pervasives_Native.uu___is_None uu___3) in
+                   if uu___2 then [id] else []
                | uu___2 -> [])
         | FStar_Parser_AST.Wild -> []
         | FStar_Parser_AST.Const uu___1 -> []
diff --git a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
index bc70ccf5b24..62f90dcdc71 100644
--- a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
+++ b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
@@ -325,10 +325,11 @@ and free_vars tvars_only env t = match (unparen t).tm with
     else (
       let ids = Ident.ids_of_lid x in
       match ids with
-      | [x] -> ( //unqualified name
-        match Env.try_lookup_id env x with
-        | None -> [x]
-        | _ -> []        
+      | [id] -> ( //unqualified name
+        if None? (Env.try_lookup_id env id)
+        && None? (Env.try_lookup_lid env x)
+        then [id]
+        else []
       )
       | _ -> []
     )