# HG changeset patch
# User wenzelm
# Date 1701873922 -3600
# Node ID 1cdc685fe8524631a997bbe148a38b3764f02dba
# Parent  810679c5ed3c39efcecf26244782bf8403ddf26f
more zproofs;

diff -r 810679c5ed3c -r 1cdc685fe852 src/Pure/thm.ML
--- 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,
diff -r 810679c5ed3c -r 1cdc685fe852 src/Pure/zterm.ML
--- 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;