tuned -- prefer high-level Table.merge with its slightly more conservative update;

--- a/src/Pure/axclass.ML	Tue Jan 08 10:34:19 2013 +0100
+++ b/src/Pure/axclass.ML	Tue Jan 08 12:39:39 2013 +0100
@@ -107,9 +107,8 @@
             params2 params1;
 
       (*see Theory.at_begin hook for transitive closure of classrels and arity completion*)
-      val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2);
-      val proven_arities' =
-        Symtab.join (K (Library.merge (eq_fst op =))) (proven_arities1, proven_arities2);
+      val proven_classrels' = Symreltab.merge (K true) (proven_classrels1, proven_classrels2);
+      val proven_arities' = Symtab.merge_list (eq_fst op =) (proven_arities1, proven_arities2);
 
       val inst_params' =
         (Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2),

--- a/src/Pure/consts.ML	Tue Jan 08 10:34:19 2013 +0100
+++ b/src/Pure/consts.ML	Tue Jan 08 12:39:39 2013 +0100
@@ -318,7 +318,7 @@
     Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
   let
     val decls' = Name_Space.merge_tables (decls1, decls2);
-    val constraints' = Symtab.join (K fst) (constraints1, constraints2);
+    val constraints' = Symtab.merge (K true) (constraints1, constraints2);
     val rev_abbrevs' = Symtab.join (K Item_Net.merge) (rev_abbrevs1, rev_abbrevs2);
   in make_consts (decls', constraints', rev_abbrevs') end;
 

--- a/src/Tools/Code/code_target.ML	Tue Jan 08 10:34:19 2013 +0100
+++ b/src/Tools/Code/code_target.ML	Tue Jan 08 12:39:39 2013 +0100
@@ -110,7 +110,7 @@
 fun merge_symbol_syntax_data
   (Symbol_Syntax_Data { class = class1, instance = instance1, tyco = tyco1, const = const1 },
     Symbol_Syntax_Data { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
-  make_symbol_syntax_data (
+  make_symbol_syntax_data ( (* FIXME proper merge order!? prefer fst!? *)
     (Symtab.join (K snd) (class1, class2),
        Symreltab.join (K snd) (instance1, instance2)),
     (Symtab.join (K snd) (tyco1, tyco2),
@@ -158,7 +158,9 @@
       module_alias = module_alias2, symbol_syntax = symbol_syntax2 }) =
   if serial1 = serial2 orelse not strict then
     make_target ((serial1, description),
-      ((merge (op =) (reserved1, reserved2), Symtab.join (K snd) (includes1, includes2)),
+      ((merge (op =) (reserved1, reserved2),
+         (* FIXME proper merge order!? prefer fst!? *)
+         Symtab.join (K snd) (includes1, includes2)),
         (Symtab.join (K snd) (module_alias1, module_alias2),
           merge_symbol_syntax_data (symbol_syntax1, symbol_syntax2))
     ))

--- a/src/Tools/adhoc_overloading.ML	Tue Jan 08 10:34:19 2013 +0100
+++ b/src/Tools/adhoc_overloading.ML	Tue Jan 08 12:39:39 2013 +0100
@@ -53,7 +53,7 @@
   fun merge
     ({internalize = int1, externalize = ext1},
       {internalize = int2, externalize = ext2}) : T =
-    {internalize = Symtab.join (K (Library.merge (op =))) (int1, int2),
+    {internalize = Symtab.merge_list (op =) (int1, int2),
       externalize = Symtab.join merge_ext (ext1, ext2)};
 );