1.1 --- a/src/HOL/Tools/meson.ML	Thu Nov 30 17:42:23 2006 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Fri Dec 01 12:23:39 2006 +0100
     1.3 @@ -210,11 +210,13 @@
     1.4    | signed_nclauses b (Const("op -->",_) $ t $ u) = 
     1.5        if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
     1.6             else sum (signed_nclauses (not b) t) (signed_nclauses b u)
     1.7 -  | signed_nclauses b (Const("op =",_) $ t $ u) = 
     1.8 -      if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
     1.9 -                    (prod (signed_nclauses (not b) u) (signed_nclauses b t))
    1.10 -           else sum (prod (signed_nclauses b t) (signed_nclauses b u))
    1.11 -                    (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
    1.12 +  | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) = 
    1.13 +      if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
    1.14 +	  if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
    1.15 +			(prod (signed_nclauses (not b) u) (signed_nclauses b t))
    1.16 +	       else sum (prod (signed_nclauses b t) (signed_nclauses b u))
    1.17 +			(prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
    1.18 +      else 1 
    1.19    | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
    1.20    | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
    1.21    | signed_nclauses _ _ = 1; (* literal *)