diff -r de95c97efab3 -r 2bb3cd36bcf7 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Sat Jan 25 22:18:20 2014 +0100
+++ b/src/Tools/Code/code_ml.ML	Sat Jan 25 23:50:49 2014 +0100
@@ -178,10 +178,9 @@
           let
             fun print_eqn definer ((ts, t), (some_thm, _)) =
               let
-                val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                 val vars = reserved
-                  |> intro_base_names
-                       (is_none o const_syntax) deresolve consts
+                  |> intro_base_names_for (is_none o const_syntax)
+                       deresolve (t :: ts)
                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
                        (insert (op =)) ts []);
                 val prolog = if needs_typ then
@@ -470,10 +469,9 @@
           let
             fun print_eqn ((ts, t), (some_thm, _)) =
               let
-                val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                 val vars = reserved
-                  |> intro_base_names
-                      (is_none o const_syntax) deresolve consts
+                  |> intro_base_names_for (is_none o const_syntax)
+                      deresolve (t :: ts)
                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
                       (insert (op =)) ts []);
               in concat [
@@ -484,10 +482,9 @@
               ] end;
             fun print_eqns is_pseudo [((ts, t), (some_thm, _))] =
                   let
-                    val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                     val vars = reserved
-                      |> intro_base_names
-                          (is_none o const_syntax) deresolve consts
+                      |> intro_base_names_for (is_none o const_syntax)
+                          deresolve (t :: ts)
                       |> intro_vars ((fold o Code_Thingol.fold_varnames)
                           (insert (op =)) ts []);
                   in
@@ -510,10 +507,9 @@
                   )
               | print_eqns _ (eqs as eq :: eqs') =
                   let
-                    val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
                     val vars = reserved
-                      |> intro_base_names
-                          (is_none o const_syntax) deresolve consts;
+                      |> intro_base_names_for (is_none o const_syntax)
+                           deresolve (map (snd o fst) eqs)
                     val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
                   in
                     Pretty.block (