# HG changeset patch
# User paulson
# Date 1164972219 -3600
# Node ID 296e0c318c3e605337f80b1429bab8f36973e957
# Parent  1bd558879c440ff5e352a77e728266e81ccc4fab
Fixed a MAJOR BUG in clause-counting: only Boolean equalities now count as iffs

diff -r 1bd558879c44 -r 296e0c318c3e src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Thu Nov 30 17:42:23 2006 +0100
+++ b/src/HOL/Tools/meson.ML	Fri Dec 01 12:23:39 2006 +0100
@@ -210,11 +210,13 @@
   | signed_nclauses b (Const("op -->",_) $ t $ u) = 
       if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
            else sum (signed_nclauses (not b) t) (signed_nclauses b u)
-  | signed_nclauses b (Const("op =",_) $ t $ u) = 
-      if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
-                    (prod (signed_nclauses (not b) u) (signed_nclauses b t))
-           else sum (prod (signed_nclauses b t) (signed_nclauses b u))
-                    (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
+  | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) = 
+      if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
+	  if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
+			(prod (signed_nclauses (not b) u) (signed_nclauses b t))
+	       else sum (prod (signed_nclauses b t) (signed_nclauses b u))
+			(prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
+      else 1 
   | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
   | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
   | signed_nclauses _ _ = 1; (* literal *)