src/Pure/thm.ML
changeset 32027 9dd548810ed1
parent 31977 e03059ae2d82
child 32032 a6a6e8031c14
     1.1 --- a/src/Pure/thm.ML	Thu Jul 16 22:58:07 2009 +0200
     1.2 +++ b/src/Pure/thm.ML	Thu Jul 16 22:58:45 2009 +0200
     1.3 @@ -1232,7 +1232,7 @@
     1.4    if i < 0 then raise THM ("negative increment", 0, [thm])
     1.5    else if i = 0 then thm
     1.6    else
     1.7 -    Thm (deriv_rule1 (Pt.map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i)) der,
     1.8 +    Thm (deriv_rule1 (Pt.incr_indexes i) der,
     1.9       {thy_ref = thy_ref,
    1.10        tags = [],
    1.11        maxidx = maxidx + i,