# HG changeset patch # User berghofe # Date 1033397040 -7200 # Node ID d4a2ac255447d94e7c875028acb1cba435d6ce36 # Parent 73c3915553b4e20d32725319657c9303f3bf6af5 Fixed bug in expand_proof which caused indexes to be incremented incorrectly. diff -r 73c3915553b4 -r d4a2ac255447 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Mon Sep 30 16:42:46 2002 +0200 +++ b/src/Pure/Proof/reconstruct.ML Mon Sep 30 16:44:00 2002 +0200 @@ -353,19 +353,22 @@ | (b, Some prop') => a = b andalso prop = prop') thms) then (maxidx, prfs, prf) else let - val (maxidx', (i, prf), prfs') = (case assoc (prfs, (a, prop)) of + fun inc i = + map_proof_terms (Logic.incr_indexes ([], i)) (incr_tvar i); + val (maxidx', i, prf, prfs') = (case assoc (prfs, (a, prop)) of None => let val _ = message ("Reconstructing proof of " ^ a); val _ = message (Sign.string_of_term sg prop); - val i = maxidx + 1; - val prf' = map_proof_terms (Logic.incr_indexes ([], i)) - (incr_tvar i) (forall_intr_vfs_prf prop - (reconstruct_proof sg prop cprf)); + val prf' = forall_intr_vfs_prf prop + (reconstruct_proof sg prop cprf); val (maxidx', prfs', prf) = expand (maxidx_of_proof prf') prfs prf' - in (maxidx', (i, prf), ((a, prop), (i, prf)) :: prfs') end - | Some p => (maxidx, p, prfs)); + in (maxidx' + maxidx + 1, maxidx + 1, inc (maxidx + 1) prf, + ((a, prop), (maxidx', prf)) :: prfs') + end + | Some (maxidx', prf) => (maxidx' + maxidx + 1, + maxidx + 1, inc (maxidx + 1) prf, prfs)); val tye = map (fn ((s, j), _) => (s, i + j)) (term_tvars prop) ~~ Ts in (maxidx', prfs',