# HG changeset patch # User wenzelm # Date 1570804116 -7200 # Node ID 55e1dd3894ce93918ca9058086557191a0d52699 # Parent 8f050cc0ec501a1cbdd452044ff0716169250f68 tuned; diff -r 8f050cc0ec50 -r 55e1dd3894ce src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Fri Oct 11 15:36:32 2019 +0200 +++ b/src/Pure/proofterm.ML Fri Oct 11 16:28:36 2019 +0200 @@ -1913,6 +1913,9 @@ fun expand_proof thy thms prf = let + fun do_expand a prop = + exists (fn (b, NONE) => a = b | (b, SOME prop') => a = b andalso prop = prop') thms; + fun expand maxidx prfs (AbsP (s, t, prf)) = let val (maxidx', prfs', prf') = expand maxidx prfs prf in (maxidx', prfs', AbsP (s, t, prf')) end @@ -1928,27 +1931,22 @@ let val (maxidx', prfs', prf') = expand maxidx prfs prf in (maxidx', prfs', prf' % t) end | expand maxidx prfs (prf as PThm ({name = a, prop, types = SOME Ts, ...}, thm_body)) = - if not (exists - (fn (b, NONE) => a = b - | (b, SOME prop') => a = b andalso prop = prop') thms) - then (maxidx, prfs, prf) else - let - val (maxidx', prf, prfs') = - (case AList.lookup (op =) prfs (a, prop) of - NONE => - let - val prf' = - thm_body_proof_open thm_body - |> reconstruct_proof thy prop - |> forall_intr_vfs_prf prop; - val (maxidx', prfs', prf) = expand (maxidx_proof prf' ~1) prfs prf' - in - (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf, - ((a, prop), (maxidx', prf)) :: prfs') - end - | SOME (maxidx', prf) => - (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf, prfs)); - in (maxidx', prfs', app_types (maxidx + 1) prop Ts prf) end + if do_expand a prop then + let + val (maxidx', prfs', prf') = + (case AList.lookup (op =) prfs (a, prop) of + NONE => + let + val prf1 = + thm_body_proof_open thm_body + |> reconstruct_proof thy prop + |> forall_intr_vfs_prf prop; + val (maxidx1, prfs1, prf2) = expand (maxidx_proof prf1 ~1) prfs prf1 + val prfs2 = ((a, prop), (maxidx1, prf2)) :: prfs1; + in (maxidx1, prfs2, incr_indexes (maxidx + 1) prf2) end + | SOME (maxidx1, prf1) => (maxidx1, prfs, incr_indexes (maxidx + 1) prf1)); + in (maxidx' + maxidx + 1, prfs', app_types (maxidx + 1) prop Ts prf') end + else (maxidx, prfs, prf) | expand maxidx prfs prf = (maxidx, prfs, prf); in #3 (expand (maxidx_proof prf ~1) [] prf) end;