permissive AList.merge -- most likely setup for theory data (beware of spurious AList.DUP);

--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Nov 15 19:44:16 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Nov 15 19:44:29 2009 +0100
@@ -189,8 +189,8 @@
   val extend = I
   fun merge ({frac_types = fs1, codatatypes = cs1},
                {frac_types = fs2, codatatypes = cs2}) : T =
-    {frac_types = AList.merge (op =) (op =) (fs1, fs2),
-     codatatypes = AList.merge (op =) (op =) (cs1, cs2)})
+    {frac_types = AList.merge (op =) (K true) (fs1, fs2),
+     codatatypes = AList.merge (op =) (K true) (cs1, cs2)})
 
 (* term * term -> term *)
 fun s_conj (t1, @{const True}) = t1

--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sun Nov 15 19:44:16 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sun Nov 15 19:44:29 2009 +0100
@@ -137,7 +137,7 @@
   val empty = {params = rev default_default_params}
   val extend = I
   fun merge ({params = ps1}, {params = ps2}) : T =
-    {params = AList.merge (op =) (op =) (ps1, ps2)})
+    {params = AList.merge (op =) (K true) (ps1, ps2)})
 
 (* raw_param -> theory -> theory *)
 fun set_default_raw_param param thy =

--- a/src/HOL/Tools/recdef.ML	Sun Nov 15 19:44:16 2009 +0100
+++ b/src/HOL/Tools/recdef.ML	Sun Nov 15 19:44:29 2009 +0100
@@ -96,7 +96,7 @@
     (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
       (Symtab.merge (K true) (tab1, tab2),
         mk_hints (Thm.merge_thms (simps1, simps2),
-          AList.merge (op =) Thm.eq_thm_prop (congs1, congs2),
+          AList.merge (op =) (K true) (congs1, congs2),
           Thm.merge_thms (wfs1, wfs2)));
 );
 

--- a/src/Tools/Code/code_preproc.ML	Sun Nov 15 19:44:16 2009 +0100
+++ b/src/Tools/Code/code_preproc.ML	Sun Nov 15 19:44:29 2009 +0100
@@ -54,6 +54,7 @@
       val pre = Simplifier.merge_ss (pre1, pre2);
       val post = Simplifier.merge_ss (post1, post2);
       val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2);
+        (* FIXME handle AList.DUP (!?) *)
     in make_thmproc ((pre, post), functrans) end;
 
 structure Code_Preproc_Data = Theory_Data