# HG changeset patch
# User wenzelm
# Date 1737581858 -3600
# Node ID 33616e13e17273ab9bfec9db0fd273ad8fededf9
# Parent  6f2bcdfa9a1940cb4b5dd6cf44b8771f364a7500
tuned signature: more operations;

diff -r 6f2bcdfa9a19 -r 33616e13e172 src/HOL/Tools/cnf.ML
--- a/src/HOL/Tools/cnf.ML	Wed Jan 22 22:22:19 2025 +0100
+++ b/src/HOL/Tools/cnf.ML	Wed Jan 22 22:37:38 2025 +0100
@@ -104,9 +104,6 @@
           (Seq.hd (REPEAT_DETERM (resolve_tac ctxt @{thms cnf.clause2raw_not_disj} i) thm))
     (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *)
     (* becomes "[..., A1, ..., An] |- B"                                   *)
-    fun prems_to_hyps thm =
-      fold (fn cprem => fn thm' =>
-        Thm.implies_elim thm' (Thm.assume cprem)) (Thm.cprems_of thm) thm
   in
     (* [...] |- ~(x1 | ... | xn) ==> False *)
     (@{thm cnf.clause2raw_notE} OF [clause])
@@ -115,7 +112,7 @@
     (* [...] |- x1' ==> ... ==> xn' ==> False *)
     |> Seq.hd o TRYALL (resolve_tac ctxt @{thms cnf.clause2raw_not_not})
     (* [..., x1', ..., xn'] |- False *)
-    |> prems_to_hyps
+    |> Thm.assume_prems ~1
   end;
 
 (* ------------------------------------------------------------------------- *)
diff -r 6f2bcdfa9a19 -r 33616e13e172 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Wed Jan 22 22:22:19 2025 +0100
+++ b/src/Pure/more_thm.ML	Wed Jan 22 22:37:38 2025 +0100
@@ -63,6 +63,7 @@
   val check_shyps: Proof.context -> thm -> thm
   val weaken_sorts': Proof.context -> cterm -> cterm
   val elim_implies: thm -> thm -> thm
+  val assume_prems: int -> thm -> thm
   val forall_intr_name: string * cterm -> thm -> thm
   val forall_elim_var: int -> thm -> thm
   val forall_elim_vars: int -> thm -> thm
@@ -334,6 +335,12 @@
 fun elim_implies thA thAB = Thm.implies_elim thAB thA;
 
 
+(* assume_prems: shift at most n premises into hyps, where n < 0 means infinity *)
+
+fun assume_prems n th =
+  fold (elim_implies o Thm.assume) (Thm.take_cprems_of n th) th;
+
+
 (* forall_intr_name *)
 
 fun forall_intr_name (a, x) th =