more zproofs;

--- a/src/Pure/thm.ML	Wed Dec 06 15:32:53 2023 +0100
+++ b/src/Pure/thm.ML	Wed Dec 06 15:45:22 2023 +0100
@@ -2023,7 +2023,7 @@
   if i < 0 then raise THM ("negative increment", 0, [thm])
   else if i = 0 then thm
   else
-    Thm (deriv_rule1 (Proofterm.incr_indexes i, ZTerm.todo_proof) der,
+    Thm (deriv_rule1 (Proofterm.incr_indexes i, ZTerm.incr_indexes_proof i) der,
      {cert = cert,
       tags = [],
       maxidx = maxidx + i,

--- a/src/Pure/zterm.ML	Wed Dec 06 15:32:53 2023 +0100
+++ b/src/Pure/zterm.ML	Wed Dec 06 15:45:22 2023 +0100
@@ -184,6 +184,7 @@
   val instantiate_proof: theory ->
     ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> zproof -> zproof
   val varifyT_proof: ((string * sort) * (indexname * sort)) list -> zproof -> zproof
+  val incr_indexes_proof: int -> zproof -> zproof
 end;
 
 structure ZTerm: ZTERM =
@@ -552,4 +553,12 @@
           | SOME w => ZTVar w));
     in Same.commit (map_proof_types_same typ) prf end;
 
+fun incr_indexes_proof inc prf =
+  let
+    fun tvar ((a, i), S) = if i >= 0 then ZTVar ((a, i + inc), S) else raise Same.SAME;
+    fun var ((x, i), T) = if i >= 0 then ZVar ((x, i + inc), T) else raise Same.SAME;
+    val typ = subst_type_same tvar;
+    val term = subst_term_same typ var;
+  in Same.commit (map_proof_same typ term) prf end;
+
 end;