src/Pure/logic.ML

--- a/src/Pure/logic.ML	Wed Jan 22 19:34:04 2025 +0100
+++ b/src/Pure/logic.ML	Wed Jan 22 21:31:45 2025 +0100
@@ -23,6 +23,7 @@
   val list_implies: term list * term -> term
   val strip_imp_prems: term -> term list
   val strip_imp_concl: term -> term
+  val take_imp_prems: int -> term -> term list
   val strip_prems: int * term list * term -> term list * term
   val count_prems: term -> int
   val no_prems: term -> bool
@@ -200,6 +201,11 @@
 fun strip_imp_concl (Const("Pure.imp", _) $ A $ B) = strip_imp_concl B
   | strip_imp_concl A = A : term;
 
+(* take at most n prems, where n < 0 means infinity *)
+fun take_imp_prems 0 _ = []
+  | take_imp_prems n (Const ("Pure.imp", _) $ A $ B) = A :: take_imp_prems (n - 1) B
+  | take_imp_prems _ _ = [];
+
 (*Strip and return premises: (i, [], A1\<Longrightarrow>...Ai\<Longrightarrow>B)
     goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED)
   if  i<0 or else i too big then raises  TERM*)