src/Tools/Code/code_ml.ML

               @@ exc_str
             )
           end
       | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
           let
-            val consts = map_filter
-              (fn c => if (is_some o syntax_const) c
-                then NONE else (SOME o Long_Name.base_name o deresolve) c)
-                (Code_Thingol.add_constnames t []);
+            val consts = Code_Thingol.add_constnames t [];
             val vars = reserved_names
-              |> Code_Printer.intro_vars consts;
+              |> Code_Printer.intro_base_names
+                  (is_none o syntax_const) deresolve consts;
           in
             concat [
               str "val",
               (str o deresolve) name,
               str ":",

                 val vs_dict = filter_out (null o snd) vs;
                 val shift = if null eqs' then I else
                   map (Pretty.block o single o Pretty.block o single);
                 fun pr_eq definer ((ts, t), (thm, _)) =
                   let
-                    val consts = map_filter
-                      (fn c => if (is_some o syntax_const) c
-                        then NONE else (SOME o Long_Name.base_name o deresolve) c)
-                        (fold Code_Thingol.add_constnames (t :: ts) []);
+                    val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                     val vars = reserved_names
-                      |> Code_Printer.intro_vars consts
+                      |> Code_Printer.intro_base_names
+                           (is_none o syntax_const) deresolve consts
                       |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
                            (insert (op =)) ts []);
                   in
                     concat (
                       str definer

               @@ exc_str
             )
           end
       | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
           let
-            val consts = map_filter
-              (fn c => if (is_some o syntax_const) c
-                then NONE else (SOME o Long_Name.base_name o deresolve) c)
-                (Code_Thingol.add_constnames t []);
+            val consts = Code_Thingol.add_constnames t [];
             val vars = reserved_names
-              |> Code_Printer.intro_vars consts;
+              |> Code_Printer.intro_base_names
+                  (is_none o syntax_const) deresolve consts;
           in
             concat [
               str "let",
               (str o deresolve) name,
               str ":",

           end
       | pr_stmt (MLFuns (funn :: funns, pseudo_funs)) =
           let
             fun pr_eq ((ts, t), (thm, _)) =
               let
-                val consts = map_filter
-                  (fn c => if (is_some o syntax_const) c
-                    then NONE else (SOME o Long_Name.base_name o deresolve) c)
-                    (fold Code_Thingol.add_constnames (t :: ts) []);
+                val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                 val vars = reserved_names
-                  |> Code_Printer.intro_vars consts
+                  |> Code_Printer.intro_base_names
+                      (is_none o syntax_const) deresolve consts
                   |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
                       (insert (op =)) ts []);
               in concat [
                 (Pretty.block o Pretty.commas)
                   (map (pr_term (member (op =) pseudo_funs) thm vars NOBR) ts),
                 str "->",
                 pr_term (member (op =) pseudo_funs) thm vars NOBR t
               ] end;
             fun pr_eqs is_pseudo [((ts, t), (thm, _))] =
                   let
-                    val consts = map_filter
-                      (fn c => if (is_some o syntax_const) c
-                        then NONE else (SOME o Long_Name.base_name o deresolve) c)
-                        (fold Code_Thingol.add_constnames (t :: ts) []);
+                    val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                     val vars = reserved_names
-                      |> Code_Printer.intro_vars consts
+                      |> Code_Printer.intro_base_names
+                          (is_none o syntax_const) deresolve consts
                       |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
                           (insert (op =)) ts []);
                   in
                     concat (
                       (if is_pseudo then [str "()"]

                     :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
                           o single o pr_eq) eqs'
                   )
               | pr_eqs _ (eqs as eq :: eqs') =
                   let
-                    val consts = map_filter
-                      (fn c => if (is_some o syntax_const) c
-                        then NONE else (SOME o Long_Name.base_name o deresolve) c)
-                        (fold Code_Thingol.add_constnames (map (snd o fst) eqs) []);
+                    val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
                     val vars = reserved_names
-                      |> Code_Printer.intro_vars consts;
+                  |> Code_Printer.intro_base_names
+                      (is_none o syntax_const) deresolve consts;
                     val dummy_parms = (map str o Code_Printer.aux_params vars o map (fst o fst)) eqs;
                   in
                     Pretty.block (
                       Pretty.breaks dummy_parms
                       @ Pretty.brk 1