# HG changeset patch
# User wenzelm
# Date 1180905417 -7200
# Node ID 492e2fd127676d7e8797ced191576a21b28a2fbf
# Parent  05fb9b2b16d73bf440c7e5bece7be8aabe4805be
monomorphic equality: let ML work out the details;

diff -r 05fb9b2b16d7 -r 492e2fd12767 src/Pure/Tools/codegen_data.ML
--- a/src/Pure/Tools/codegen_data.ML	Sun Jun 03 23:16:56 2007 +0200
+++ b/src/Pure/Tools/codegen_data.ML	Sun Jun 03 23:16:57 2007 +0200
@@ -211,7 +211,7 @@
   in (SOME consts, thms) end;
 
 val eq_string = op = : string * string -> bool;
-val eq_co = eq_pair eq_string (eq_list (is_equal o Term.typ_ord));
+val eq_co = op = : (string * typ list) * (string * typ list) -> bool;
 fun eq_dtyp ((vs1, cs1), (vs2, cs2)) = 
   gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2)
     andalso gen_eq_set eq_co (cs1, cs2);
diff -r 05fb9b2b16d7 -r 492e2fd12767 src/Pure/Tools/codegen_names.ML
--- a/src/Pure/Tools/codegen_names.ML	Sun Jun 03 23:16:56 2007 +0200
+++ b/src/Pure/Tools/codegen_names.ML	Sun Jun 03 23:16:57 2007 +0200
@@ -232,14 +232,12 @@
 
 type tyco = string;
 type const = string;
-val string_pair_ord = prod_ord fast_string_ord fast_string_ord;
-val eq_string_pair = is_equal o string_pair_ord;
 structure Consttab = CodegenConsts.Consttab;
 
 structure StringPairTab =
   TableFun(
     type key = string * string;
-    val ord = string_pair_ord;
+    val ord = prod_ord fast_string_ord fast_string_ord;
   );
 
 datatype names = Names of {
@@ -256,8 +254,6 @@
   instance = (StringPairTab.empty, Symtab.empty)
 };
 
-val eq_string = op = : string * string -> bool;
-
 local
   fun mk_names (class, classrel, tyco, instance) =
     Names { class = class, classrel = classrel, tyco = tyco, instance = instance };
@@ -270,10 +266,10 @@
     Names { class = (class2, classrev2),
       classrel = (classrel2, classrelrev2), tyco = (tyco2, tycorev2),
       instance = (instance2, instancerev2) }) =
-    mk_names ((Symtab.merge eq_string (class1, class2), Symtab.merge eq_string (classrev1, classrev2)),
-      (StringPairTab.merge eq_string (classrel1, classrel2), Symtab.merge eq_string_pair (classrelrev1, classrelrev2)),
-      (Symtab.merge eq_string (tyco1, tyco2), Symtab.merge eq_string (tycorev1, tycorev2)),
-      (StringPairTab.merge eq_string (instance1, instance2), Symtab.merge eq_string_pair (instancerev1, instancerev2)));
+    mk_names ((Symtab.merge (op =) (class1, class2), Symtab.merge (op =) (classrev1, classrev2)),
+      (StringPairTab.merge (op =) (classrel1, classrel2), Symtab.merge (op =) (classrelrev1, classrelrev2)),
+      (Symtab.merge (op =) (tyco1, tyco2), Symtab.merge (op =) (tycorev1, tycorev2)),
+      (StringPairTab.merge (op =) (instance1, instance2), Symtab.merge (op =) (instancerev1, instancerev2)));
   fun map_class f = map_names
     (fn (class, classrel, tyco, inst) => (f class, classrel, tyco, inst));
   fun map_classrel f = map_names
@@ -297,8 +293,8 @@
 (
   type T = const Consttab.table * (string * string option) Symtab.table;
   val empty = (Consttab.empty, Symtab.empty);
-  fun merge _ ((const1, constrev1), (const2, constrev2)) =
-    (Consttab.merge eq_string (const1, const2),
+  fun merge _ ((const1, constrev1), (const2, constrev2)) : T =
+    (Consttab.merge (op =) (const1, const2),
       Symtab.merge CodegenConsts.eq_const (constrev1, constrev2));
   fun purge _ NONE _ = empty
     | purge _ (SOME cs) (const, constrev) = (fold Consttab.delete_safe cs const,