# HG changeset patch
# User wenzelm
# Date 1702204977 -3600
# Node ID a8db9ee24d5eb0a59ecb90f8d3cd1024fec2ca24
# Parent  0b87e04d0b6850f8ae2f011b33b88163e0a6e4f5
clarified signature;
minor performance tuning;

diff -r 0b87e04d0b68 -r a8db9ee24d5e src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sun Dec 10 11:24:42 2023 +0100
+++ b/src/Pure/proofterm.ML	Sun Dec 10 11:42:57 2023 +0100
@@ -128,7 +128,7 @@
   val permute_prems_proof: term list -> int -> int -> proof -> proof
   val generalize_proof: Names.set * Names.set -> int -> term -> proof -> proof
   val instantiate: typ TVars.table * term Vars.table -> proof -> proof
-  val lift_proof: term -> int -> term -> proof -> proof
+  val lift_proof: term -> int -> term list -> proof -> proof
   val incr_indexes: int -> proof -> proof
   val assumption_proof: term list -> term -> int -> proof -> proof
   val bicompose_proof: bool -> term list -> term list -> term option -> term list ->
@@ -1015,7 +1015,7 @@
 
 (* lifting *)
 
-fun lift_proof Bi inc prop prf =
+fun lift_proof gprop inc prems prf =
   let
     val typ = Logic.incr_tvar_same inc;
     val typs = Same.map_option (Same.map typ);
@@ -1042,11 +1042,10 @@
           PThm (thm_header serial pos theory_name name prop (typs types), thm_body)
       | proof _ _ _ = raise Same.SAME;
 
-    val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop);
-    val k = length ps;
+    val k = length prems;
 
-    fun mk_app b (i, j, prf) =
-      if b then (i - 1, j, prf %% PBound i) else (i, j - 1, prf %> Bound j);
+    fun mk_app b (i, j, p) =
+      if b then (i - 1, j, p %% PBound i) else (i, j - 1, p %> Bound j);
 
     fun lift Us bs i j (Const ("Pure.imp", _) $ A $ B) =
           AbsP ("H", NONE (*A*), lift Us (true::bs) (i + 1) j B)
@@ -1055,7 +1054,7 @@
       | lift Us bs i j _ =
           proof_combP (Same.commit (proof (rev Us) []) prf,
             map (fn k => (#3 (fold_rev mk_app bs (i - 1, j - 1, PBound k)))) (i + k - 1 downto i));
-  in mk_AbsP ps (lift [] [] 0 0 Bi) end;
+  in mk_AbsP prems (lift [] [] 0 0 gprop) end;
 
 fun incr_indexes i =
   Same.commit (map_proof_terms_same
diff -r 0b87e04d0b68 -r a8db9ee24d5e src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Dec 10 11:24:42 2023 +0100
+++ b/src/Pure/thm.ML	Sun Dec 10 11:42:57 2023 +0100
@@ -2029,8 +2029,9 @@
     if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, [])
     else
       let
+        val prems = map lift_all As;
         fun zproof p = ZTerm.todo_proof p;
-        fun proof p = Proofterm.lift_proof gprop inc prop p;
+        fun proof p = Proofterm.lift_proof gprop inc prems p;
       in
         Thm (deriv_rule1 zproof proof der,
          {cert = join_certificate1 (goal, orule),
@@ -2040,7 +2041,7 @@
           shyps = Sorts.union shyps sorts,  (*sic!*)
           hyps = hyps,
           tpairs = map (apply2 lift_abs) tpairs,
-          prop = Logic.list_implies (map lift_all As, lift_all B)})
+          prop = Logic.list_implies (prems, lift_all B)})
       end
   end;