src/Tools/Code/code_ml.ML
changeset 42599 1a82b0400b2a
parent 41952 c7297638599b
child 43326 47cf4bc789aa
child 43343 e83695ea0e0a
--- a/src/Tools/Code/code_ml.ML	Mon May 02 10:50:07 2011 +0200
+++ b/src/Tools/Code/code_ml.ML	Mon May 02 10:50:09 2011 +0200
@@ -483,6 +483,8 @@
               let
                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                 val vars = reserved
+                  |> intro_base_names
+                      (is_none o const_syntax) deresolve consts
                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
                       (insert (op =)) ts []);
               in concat [