diff -r 89463ae2612d -r 8c11b1ce2f05 src/HOL/Tools/cnf_funcs.ML
--- a/src/HOL/Tools/cnf_funcs.ML	Wed Nov 29 04:11:06 2006 +0100
+++ b/src/HOL/Tools/cnf_funcs.ML	Wed Nov 29 04:11:09 2006 +0100
@@ -540,7 +540,7 @@
 	(* remove the original premises *)
 	THEN SELECT_GOAL (fn thm =>
 		let
-			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm, 0)
+			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
 		in
 			PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
 		end) i;
@@ -564,7 +564,7 @@
 	(* remove the original premises *)
 	THEN SELECT_GOAL (fn thm =>
 		let
-			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm, 0)
+			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
 		in
 			PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
 		end) i;