src/Tools/Code/code_ml.ML

       | 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.fold_constnames (insert (op =)) t []);
+                (Code_Thingol.add_constnames t []);
             val vars = reserved_names
               |> Code_Printer.intro_vars consts;
           in
             concat [
               str "val",

                 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 o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
+                        (fold Code_Thingol.add_constnames (t :: ts) []);
                     val vars = reserved_names
                       |> Code_Printer.intro_vars consts
-                      |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+                      |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
                            (insert (op =)) ts []);
                   in
                     concat (
                       str definer
                       :: (str o deresolve) name

       | 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.fold_constnames (insert (op =)) t []);
+                (Code_Thingol.add_constnames t []);
             val vars = reserved_names
               |> Code_Printer.intro_vars consts;
           in
             concat [
               str "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 o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
+                    (fold Code_Thingol.add_constnames (t :: ts) []);
                 val vars = reserved_names
                   |> Code_Printer.intro_vars consts
-                  |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+                  |> 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 "->",

             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 o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
+                        (fold Code_Thingol.add_constnames (t :: ts) []);
                     val vars = reserved_names
                       |> Code_Printer.intro_vars consts
-                      |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+                      |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
                           (insert (op =)) ts []);
                   in
                     concat (
                       (if is_pseudo then [str "()"]
                         else map (pr_term (member (op =) pseudo_funs) thm vars BR) ts)

               | 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 o Code_Thingol.fold_constnames)
-                          (insert (op =)) (map (snd o fst) eqs) []);
+                        (fold Code_Thingol.add_constnames (map (snd o fst) eqs) []);
                     val vars = reserved_names
                       |> Code_Printer.intro_vars consts;
                     val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
                   in
                     Pretty.block (

       let
         val eqs = filter (snd o snd) raw_eqs;
         val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
          of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
             then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), thm)], false)
-            else (eqs, not (Code_Thingol.fold_constnames
-              (fn name' => fn b => b orelse name = name') t false))
+            else (eqs, not (member (op =) (Code_Thingol.add_constnames t []) name))
           | _ => (eqs, false)
           else (eqs, false)
       in ((name, (tysm, eqs')), is_value) end;
     fun check_kind [((name, (tysm, [(([], t), thm)])), true)] = MLVal (name, ((tysm, t), thm))
       | check_kind [((name, ((vs, ty), [])), _)] =