proper ZTerm.lift_proof (amending 4a1a25bdf81d);

--- a/src/Pure/thm.ML	Sun Dec 10 18:27:53 2023 +0100
+++ b/src/Pure/thm.ML	Mon Dec 11 11:46:12 2023 +0100
@@ -2029,12 +2029,13 @@
     if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, [])
     else
       let
+        val cert = join_certificate1 (goal, orule);
         val prems = map lift_all As;
-        fun zproof p = ZTerm.todo_proof p;
+        fun zproof p = ZTerm.lift_proof (Context.certificate_theory cert) gprop inc prems p;
         fun proof p = Proofterm.lift_proof gprop inc prems p;
       in
         Thm (deriv_rule1 zproof proof der,
-         {cert = join_certificate1 (goal, orule),
+         {cert = cert,
           tags = [],
           maxidx = maxidx + inc,
           constraints = constraints,

--- a/src/Pure/zterm.ML	Sun Dec 10 18:27:53 2023 +0100
+++ b/src/Pure/zterm.ML	Mon Dec 11 11:46:12 2023 +0100
@@ -203,7 +203,7 @@
     term list -> int -> zproof -> zproof
   val permute_prems_proof: theory -> term list -> int -> int -> zproof -> zproof
   val incr_indexes_proof: int -> zproof -> zproof
-  val lift_proof: theory -> term -> int -> zterm list -> zproof -> zproof
+  val lift_proof: theory -> term -> int -> term list -> zproof -> zproof
   val assumption_proof: theory -> Envir.env -> term list -> term -> int -> zproof -> zproof
 end;
 
@@ -852,7 +852,7 @@
       | lift Ts bs i j _ =
           ZAppps (Same.commit (proof (rev Ts) 0) prf,
             map (fn k => (#3 (fold_rev mk_app bs (i - 1, j - 1, ZBoundp k)))) (i + k - 1 downto i));
-  in ZAbsps prems (lift [] [] 0 0 gprop) end;
+  in ZAbsps (map zterm prems) (lift [] [] 0 0 gprop) end;
 
 
 (* higher-order resolution *)