--- 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 *****)
--- a/src/Pure/thm.ML Thu Jul 16 22:58:07 2009 +0200
+++ b/src/Pure/thm.ML Thu Jul 16 22:58:45 2009 +0200
@@ -1232,7 +1232,7 @@
if i < 0 then raise THM ("negative increment", 0, [thm])
else if i = 0 then thm
else
- Thm (deriv_rule1 (Pt.map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i)) der,
+ Thm (deriv_rule1 (Pt.incr_indexes i) der,
{thy_ref = thy_ref,
tags = [],
maxidx = maxidx + i,