src/Pure/zterm.ML

     zproof -> zproof -> zproof
   val generalize_proof: Names.set * Names.set -> int -> zproof -> zproof
   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 =
 struct
 

           (case ZTVars.lookup tab v of
             NONE => raise Same.SAME
           | SOME w => ZTVar w));
     in Same.commit (map_proof_types_same typ) prf end;
 
-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;