# HG changeset patch
# User haftmann
# Date 1246632667 -7200
# Node ID 004c9a18e69921a2bba59d9ca3dc24edc82d1c59
# Parent  cd65110353156fae2f07d08daca05e60e8b75507
cleaned up fundamental iml term functions

diff -r cd6511035315 -r 004c9a18e699 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Fri Jul 03 16:51:06 2009 +0200
+++ b/src/Tools/Code/code_haskell.ML	Fri Jul 03 16:51:07 2009 +0200
@@ -147,10 +147,10 @@
                 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 = init_syms
                   |> 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
                 semicolon (
diff -r cd6511035315 -r 004c9a18e699 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Fri Jul 03 16:51:06 2009 +0200
+++ b/src/Tools/Code/code_ml.ML	Fri Jul 03 16:51:07 2009 +0200
@@ -178,7 +178,7 @@
             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
@@ -203,10 +203,10 @@
                     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 (
@@ -488,7 +488,7 @@
             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
@@ -508,10 +508,10 @@
                 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)
@@ -524,10 +524,10 @@
                     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 (
@@ -552,8 +552,7 @@
                     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;
@@ -777,8 +776,7 @@
         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;