# HG changeset patch # User wenzelm # Date 1681811104 -7200 # Node ID 6f7a577a1406ed3d711dae25b5fd7369af18fe9a # Parent 11e8f27e741a395192b472bcba54c79e81fec34a Backed out changeset e3db27e3b0c6 diff -r 11e8f27e741a -r 6f7a577a1406 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Tue Apr 18 11:44:10 2023 +0200 +++ b/src/Pure/proofterm.ML Tue Apr 18 11:45:04 2023 +0200 @@ -42,6 +42,7 @@ type thm = serial * thm_node type thms = thm_node PThms.table val union_thms: thms * thms -> thms + val unions_thms: thms list -> thms exception MIN_PROOF of unit val proof_of: proof_body -> proof val join_proof: proof_body future -> proof @@ -237,6 +238,7 @@ type thms = thm_node PThms.table; val union_thms: thms * thms -> thms = PThms.merge (K true); +val unions_thms: thms list -> thms = PThms.merges (K true); exception MIN_PROOF of unit; @@ -1992,8 +1994,13 @@ val _ = consolidate_bodies (map #2 ps @ [body0]); val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0; val oracles = - fold (fn (_, PBody {oracles, ...}) => fn acc => Oracles.merge (acc, oracles)) ps oracles0; - val thms = fold (fn (_, PBody {thms, ...}) => fn acc => union_thms (acc, thms)) ps thms0; + Oracles.merges + (fold (fn (_, PBody {oracles, ...}) => not (Oracles.is_empty oracles) ? cons oracles) + ps [oracles0]); + val thms = + unions_thms + (fold (fn (_, PBody {thms, ...}) => not (PThms.is_empty thms) ? cons thms) + ps [thms0]); val proof = rew_proof thy proof0; in PBody {oracles = oracles, thms = thms, proof = proof} end;