--- a/src/Pure/proofterm.ML Thu Jul 16 22:58:07 2009 +0200
+++ b/src/Pure/proofterm.ML Thu Jul 16 22:58:45 2009 +0200
@@ -88,6 +88,7 @@
val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
-> proof -> proof
val lift_proof: term -> int -> term -> proof -> proof
+ val incr_indexes: int -> proof -> proof
val assumption_proof: term list -> term -> int -> proof -> proof
val bicompose_proof: bool -> term list -> term list -> term list -> term option ->
int -> int -> proof -> proof -> proof
@@ -747,6 +748,11 @@
mk_AbsP (k, lift [] [] 0 0 Bi)
end;
+fun incr_indexes i =
+ map_proof_terms_option
+ (Same.capture (Logic.incr_indexes_same ([], i)))
+ (Same.capture (Logic.incr_tvar_same i));
+
(***** proof by assumption *****)