src/Tools/Code/code_ml.ML
changeset 32913 3e9809678574
parent 32908 9aa8dfef16ff
child 32924 d2e9b2dab760
--- a/src/Tools/Code/code_ml.ML	Mon Oct 12 14:22:54 2009 +0200
+++ b/src/Tools/Code/code_ml.ML	Mon Oct 12 15:46:38 2009 +0200
@@ -175,12 +175,10 @@
           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",
@@ -200,12 +198,10 @@
                   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
@@ -472,12 +468,10 @@
           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",
@@ -492,12 +486,10 @@
           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 [
@@ -508,12 +500,10 @@
               ] 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
@@ -536,12 +526,10 @@
                   )
               | 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 (