--- a/src/Pure/proofterm.ML Tue Apr 11 20:52:38 2023 +0200
+++ b/src/Pure/proofterm.ML Tue Apr 11 21:02:15 2023 +0200
@@ -41,7 +41,7 @@
proof: proof}
type thm = serial * thm_node
type thms = thm_node PThms.table
- val union_thms: thms * thms -> thms
+ val merge_thms: thms * thms -> thms
exception MIN_PROOF of unit
val proof_of: proof_body -> proof
val join_proof: proof_body future -> proof
@@ -236,7 +236,7 @@
type thm = serial * thm_node;
type thms = thm_node PThms.table;
-val union_thms: thms * thms -> thms = PThms.merge (K true);
+val merge_thms: thms * thms -> thms = PThms.merge (K true);
exception MIN_PROOF of unit;
@@ -1993,7 +1993,7 @@
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;
+ val thms = fold (fn (_, PBody {thms, ...}) => fn acc => merge_thms (acc, thms)) ps thms0;
val proof = rew_proof thy proof0;
in PBody {oracles = oracles, thms = thms, proof = proof} end;
--- a/src/Pure/thm.ML Tue Apr 11 20:52:38 2023 +0200
+++ b/src/Pure/thm.ML Tue Apr 11 21:02:15 2023 +0200
@@ -753,7 +753,7 @@
let
val ps = merge_promises (promises1, promises2);
val oracles = Oracles.merge (oracles1, oracles2);
- val thms = Proofterm.union_thms (thms1, thms2);
+ val thms = Proofterm.merge_thms (thms1, thms2);
val prf =
(case ! Proofterm.proofs of
2 => f prf1 prf2
@@ -974,7 +974,7 @@
local
fun union_digest (oracles1, thms1) (oracles2, thms2) =
- (Oracles.merge (oracles1, oracles2), Proofterm.union_thms (thms1, thms2));
+ (Oracles.merge (oracles1, oracles2), Proofterm.merge_thms (thms1, thms2));
fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) =
(oracles, thms);