src/Pure/logic.ML

   val list_implies      : term list * term -> term
   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 nth_prem		: int * term -> term
   val mk_conjunction    : term * term -> term
   val mk_conjunction_list: term list -> term
   val strip_horn        : term -> term list * term
   val mk_cond_defpair   : term list -> term * term -> string * term
   val mk_defpair        : term * term -> string * term

 fun strip_prems (0, As, B) = (As, B)
   | strip_prems (i, As, Const("==>", _) $ A $ B) =
         strip_prems (i-1, A::As, B)
   | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
 
-(*Count premises -- quicker than (length ostrip_prems) *)
+(*Count premises -- quicker than (length o strip_prems) *)
 fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1)
   | count_prems (_,n) = n;
+
+(*Select Ai from A1 ==>...Ai==>B*)
+fun nth_prem (1, Const ("==>", _) $ A $ _) = A
+  | nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B)
+  | nth_prem (_, A) = raise TERM ("nth_prem", [A]);
 
 (*strip a proof state (Horn clause):
   B1 ==> ... Bn ==> C   goes to   ([B1, ..., Bn], C)    *)
 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);