src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 33699 f33b036ef318
parent 33583 b5e0909cd5ea
child 33701 9dd1079cec3a
--- 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