# HG changeset patch
# User wenzelm
# Date 1247777925 -7200
# Node ID 9dd548810ed1d5aa042f6a0c6cc91b938b6f89f7
# Parent  9898880061dfc3375a9383499b882b54f3d41d8a
tuned incr_indexes;

diff -r 9898880061df -r 9dd548810ed1 src/Pure/proofterm.ML
--- 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 *****)
 
diff -r 9898880061df -r 9dd548810ed1 src/Pure/thm.ML
--- 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,