more zproofs, imitating existing proofs (which are a bit rough here);

--- a/src/Pure/thm.ML	Wed Dec 13 19:55:50 2023 +0100
+++ b/src/Pure/thm.ML	Wed Dec 13 19:58:26 2023 +0100
@@ -2263,6 +2263,19 @@
     if Symtab.forall (op =) vars andalso Symtab.forall (op =) bounds then NONE
     else
       let
+        fun zterm (ZVar ((x, i), T)) =
+              if i >= 0 then
+                let val y = perhaps (Symtab.lookup vars) x
+                in if x = y then raise Same.SAME else ZVar ((y, i), T) end
+              else raise Same.SAME
+          | zterm (ZAbs (x, T, t)) =
+              let val y = perhaps (Symtab.lookup bounds) x
+              in if x = y then ZAbs (x, T, zterm t) else ZAbs (y, T, Same.commit zterm t) end
+          | zterm (ZApp (t, u)) =
+              (ZApp (zterm t, Same.commit zterm u)
+                handle Same.SAME => ZApp (t, zterm u))
+          | zterm _ = raise Same.SAME;
+
         fun term (Var ((x, i), T)) =
               let val y = perhaps (Symtab.lookup vars) x
               in if x = y then raise Same.SAME else Var ((y, i), T) end
@@ -2271,7 +2284,8 @@
               in if x = y then Abs (x, T, term t) else Abs (y, T, Same.commit term t) end
           | term (t $ u) = (term t $ Same.commit term u handle Same.SAME => t $ term u)
           | term _ = raise Same.SAME;
-      in SOME term end
+
+      in SOME {zterm = zterm, term = term} end
   end;
 
 
@@ -2379,11 +2393,11 @@
       let val (As1, rder') =
         if lifted then
           (case rename_bvars dpairs tpairs B As0 of
-            SOME f =>
+            SOME {zterm, term} =>
               let
-                fun proof p = Same.commit (Proofterm.map_proof_terms_same f I) p;
-                fun zproof p = ZTerm.todo_proof p;
-              in (map (strip_apply (Same.commit f) B) As0, deriv_rule1 zproof proof rder) end
+                fun zproof p = Same.commit (ZTerm.map_proof_same Same.same zterm) p;
+                fun proof p = Same.commit (Proofterm.map_proof_terms_same term I) p;
+              in (map (strip_apply (Same.commit term) B) As0, deriv_rule1 zproof proof rder) end
           | NONE => (As0, rder))
         else (As0, rder);
       in