src/HOL/Tools/cnf_funcs.ML
changeset 21576 8c11b1ce2f05
parent 20547 796ae7fa1049
child 24958 ff15f76741bd
     1.1 --- a/src/HOL/Tools/cnf_funcs.ML	Wed Nov 29 04:11:06 2006 +0100
     1.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Wed Nov 29 04:11:09 2006 +0100
     1.3 @@ -540,7 +540,7 @@
     1.4  	(* remove the original premises *)
     1.5  	THEN SELECT_GOAL (fn thm =>
     1.6  		let
     1.7 -			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm, 0)
     1.8 +			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
     1.9  		in
    1.10  			PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
    1.11  		end) i;
    1.12 @@ -564,7 +564,7 @@
    1.13  	(* remove the original premises *)
    1.14  	THEN SELECT_GOAL (fn thm =>
    1.15  		let
    1.16 -			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm, 0)
    1.17 +			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
    1.18  		in
    1.19  			PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
    1.20  		end) i;