src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 33699 f33b036ef318
parent 33574 b5e0909cd5ea
child 33701 9dd1079cec3a
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Nov 15 19:44:16 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Nov 15 19:44:29 2009 +0100
     1.3 @@ -189,8 +189,8 @@
     1.4    val extend = I
     1.5    fun merge ({frac_types = fs1, codatatypes = cs1},
     1.6                 {frac_types = fs2, codatatypes = cs2}) : T =
     1.7 -    {frac_types = AList.merge (op =) (op =) (fs1, fs2),
     1.8 -     codatatypes = AList.merge (op =) (op =) (cs1, cs2)})
     1.9 +    {frac_types = AList.merge (op =) (K true) (fs1, fs2),
    1.10 +     codatatypes = AList.merge (op =) (K true) (cs1, cs2)})
    1.11  
    1.12  (* term * term -> term *)
    1.13  fun s_conj (t1, @{const True}) = t1