# HG changeset patch
# User wenzelm
# Date 1247778732 -7200
# Node ID 47122b809e3785a06d4091cc7c072351173d428d
# Parent  9dd548810ed1d5aa042f6a0c6cc91b938b6f89f7
incr_indexes (from Proofterm);

diff -r 9dd548810ed1 -r 47122b809e37 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Thu Jul 16 22:58:45 2009 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Thu Jul 16 23:12:12 2009 +0200
@@ -353,8 +353,6 @@
               | (b, SOME prop') => a = b andalso prop = prop') thms)
           then (maxidx, prfs, prf) else
           let
-            fun inc i =
-              map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i);
             val (maxidx', prf, prfs') =
               (case AList.lookup (op =) prfs (a, prop) of
                 NONE =>
@@ -365,11 +363,11 @@
                       (reconstruct_proof thy prop (join_proof body));
                     val (maxidx', prfs', prf) = expand
                       (maxidx_proof prf' ~1) prfs prf'
-                  in (maxidx' + maxidx + 1, inc (maxidx + 1) prf,
+                  in (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf,
                     ((a, prop), (maxidx', prf)) :: prfs')
                   end
               | SOME (maxidx', prf) => (maxidx' + maxidx + 1,
-                  inc (maxidx + 1) prf, prfs));
+                  incr_indexes (maxidx + 1) prf, prfs));
             val tfrees = OldTerm.term_tfrees prop;
             val tye = map (fn ((s, j), _) => (s, maxidx + 1 + j))
               (OldTerm.term_tvars prop) @ map (rpair ~1 o fst) tfrees ~~ Ts;