# HG changeset patch
# User wenzelm
# Date 1258310669 -3600
# Node ID f33b036ef3183a7462ee5c0080e088d3ecee4b47
# Parent  b5f36fa5a7b4b482cf401d8f21637cf14a55e27c
permissive AList.merge -- most likely setup for theory data (beware of spurious AList.DUP);

diff -r b5f36fa5a7b4 -r f33b036ef318 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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
diff -r b5f36fa5a7b4 -r f33b036ef318 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- 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 =
diff -r b5f36fa5a7b4 -r f33b036ef318 src/HOL/Tools/recdef.ML
--- 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)));
 );
 
diff -r b5f36fa5a7b4 -r f33b036ef318 src/Tools/Code/code_preproc.ML
--- 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