src/Pure/logic.ML
changeset 21576 8c11b1ce2f05
parent 21520 63c73f461eec
child 22893 1b0f4e6f81aa
     1.1 --- a/src/Pure/logic.ML	Wed Nov 29 04:11:06 2006 +0100
     1.2 +++ b/src/Pure/logic.ML	Wed Nov 29 04:11:09 2006 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4    val strip_imp_prems: term -> term list
     1.5    val strip_imp_concl: term -> term
     1.6    val strip_prems: int * term list * term -> term list * term
     1.7 -  val count_prems: term * int -> int
     1.8 +  val count_prems: term -> int
     1.9    val nth_prem: int * term -> term
    1.10    val conjunction: term
    1.11    val mk_conjunction: term * term -> term
    1.12 @@ -137,8 +137,8 @@
    1.13    | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
    1.14  
    1.15  (*Count premises -- quicker than (length o strip_prems) *)
    1.16 -fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1)
    1.17 -  | count_prems (_,n) = n;
    1.18 +fun count_prems (Const ("==>", _) $ _ $ B) = 1 + count_prems B
    1.19 +  | count_prems _ = 0;
    1.20  
    1.21  (*Select Ai from A1 ==>...Ai==>B*)
    1.22  fun nth_prem (1, Const ("==>", _) $ A $ _) = A