# HG changeset patch
# User wenzelm
# Date 1164769869 -3600
# Node ID 8c11b1ce2f051fb1294b1884c8f783fe73369096
# Parent  89463ae2612da3e01ad4b4d49b5ce2ccf13e0aa3
simplified Logic.count_prems;

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;
diff -r 89463ae2612d -r 8c11b1ce2f05 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Wed Nov 29 04:11:06 2006 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Wed Nov 29 04:11:09 2006 +0100
@@ -137,7 +137,7 @@
 fun make is_open rule_struct (thy, prop) cases =
   let
     val n = length cases;
-    val nprems = Logic.count_prems (prop, 0);
+    val nprems = Logic.count_prems prop;
     fun add_case (name, concls) (cs, i) =
       ((case try (fn () =>
           (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
diff -r 89463ae2612d -r 8c11b1ce2f05 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Wed Nov 29 04:11:06 2006 +0100
+++ b/src/Pure/logic.ML	Wed Nov 29 04:11:09 2006 +0100
@@ -18,7 +18,7 @@
   val strip_imp_prems: term -> term list
   val strip_imp_concl: term -> term
   val strip_prems: int * term list * term -> term list * term
-  val count_prems: term * int -> int
+  val count_prems: term -> int
   val nth_prem: int * term -> term
   val conjunction: term
   val mk_conjunction: term * term -> term
@@ -137,8 +137,8 @@
   | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
 
 (*Count premises -- quicker than (length o strip_prems) *)
-fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1)
-  | count_prems (_,n) = n;
+fun count_prems (Const ("==>", _) $ _ $ B) = 1 + count_prems B
+  | count_prems _ = 0;
 
 (*Select Ai from A1 ==>...Ai==>B*)
 fun nth_prem (1, Const ("==>", _) $ A $ _) = A
diff -r 89463ae2612d -r 8c11b1ce2f05 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Wed Nov 29 04:11:06 2006 +0100
+++ b/src/Pure/meta_simplifier.ML	Wed Nov 29 04:11:09 2006 +0100
@@ -856,7 +856,7 @@
                           else Thm.cterm_match (elhs', eta_t');
         val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
         val prop' = Thm.prop_of thm';
-        val unconditional = (Logic.count_prems (prop',0) = 0);
+        val unconditional = (Logic.count_prems prop' = 0);
         val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
       in
         if perm andalso not (termless (rhs', lhs'))
diff -r 89463ae2612d -r 8c11b1ce2f05 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Nov 29 04:11:06 2006 +0100
+++ b/src/Pure/thm.ML	Wed Nov 29 04:11:09 2006 +0100
@@ -500,7 +500,7 @@
 
 val concl_of = Logic.strip_imp_concl o prop_of;
 val prems_of = Logic.strip_imp_prems o prop_of;
-fun nprems_of th = Logic.count_prems (prop_of th, 0);
+val nprems_of = Logic.count_prems o prop_of;
 fun no_prems th = nprems_of th = 0;
 
 fun major_prem_of th =
@@ -1506,8 +1506,7 @@
      and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps,
              tpairs=rtpairs, prop=rprop,...} = orule
          (*How many hyps to skip over during normalization*)
-     and nlift = Logic.count_prems(strip_all_body Bi,
-                                   if eres_flg then ~1 else 0)
+     and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0)
      val thy_ref = merge_thys2 state orule;
      val thy = Theory.deref thy_ref;
      (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)