Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/logic.ML
changeset 21576 8c11b1ce2f05
parent 21520 63c73f461eec
child 22893 1b0f4e6f81aa 
--- 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
isabelle