tuned incr_indexes;
authorwenzelm
Thu Jul 16 22:58:45 2009 +0200 (2009-07-16)
changeset 320279dd548810ed1
parent 32026 9898880061df
child 32028 47122b809e37
tuned incr_indexes;
src/Pure/proofterm.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/proofterm.ML	Thu Jul 16 22:58:07 2009 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Thu Jul 16 22:58:45 2009 +0200
     1.3 @@ -88,6 +88,7 @@
     1.4    val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
     1.5      -> proof -> proof
     1.6    val lift_proof: term -> int -> term -> proof -> proof
     1.7 +  val incr_indexes: int -> proof -> proof
     1.8    val assumption_proof: term list -> term -> int -> proof -> proof
     1.9    val bicompose_proof: bool -> term list -> term list -> term list -> term option ->
    1.10      int -> int -> proof -> proof -> proof
    1.11 @@ -747,6 +748,11 @@
    1.12      mk_AbsP (k, lift [] [] 0 0 Bi)
    1.13    end;
    1.14  
    1.15 +fun incr_indexes i =
    1.16 +  map_proof_terms_option
    1.17 +    (Same.capture (Logic.incr_indexes_same ([], i)))
    1.18 +    (Same.capture (Logic.incr_tvar_same i));
    1.19 +
    1.20  
    1.21  (***** proof by assumption *****)
    1.22  
     2.1 --- a/src/Pure/thm.ML	Thu Jul 16 22:58:07 2009 +0200
     2.2 +++ b/src/Pure/thm.ML	Thu Jul 16 22:58:45 2009 +0200
     2.3 @@ -1232,7 +1232,7 @@
     2.4    if i < 0 then raise THM ("negative increment", 0, [thm])
     2.5    else if i = 0 then thm
     2.6    else
     2.7 -    Thm (deriv_rule1 (Pt.map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i)) der,
     2.8 +    Thm (deriv_rule1 (Pt.incr_indexes i) der,
     2.9       {thy_ref = thy_ref,
    2.10        tags = [],
    2.11        maxidx = maxidx + i,