# HG changeset patch
# User wenzelm
# Date 1681811050 -7200
# Node ID 11e8f27e741a395192b472bcba54c79e81fec34a
# Parent  760515c45864239e15e40647942f573d9b81d05d
Backed out changeset cd5d56abda10

diff -r 760515c45864 -r 11e8f27e741a src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Apr 17 23:32:46 2023 +0200
+++ b/src/Pure/proofterm.ML	Tue Apr 18 11:44:10 2023 +0200
@@ -41,7 +41,7 @@
      proof: proof}
   type thm = serial * thm_node
   type thms = thm_node PThms.table
-  val merge_thms: thms * thms -> thms
+  val union_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 merge_thms: thms * thms -> thms = PThms.merge (K true);
+val union_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 => merge_thms (acc, thms)) ps thms0;
+    val thms = fold (fn (_, PBody {thms, ...}) => fn acc => union_thms (acc, thms)) ps thms0;
     val proof = rew_proof thy proof0;
   in PBody {oracles = oracles, thms = thms, proof = proof} end;
 
diff -r 760515c45864 -r 11e8f27e741a src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Apr 17 23:32:46 2023 +0200
+++ b/src/Pure/thm.ML	Tue Apr 18 11:44:10 2023 +0200
@@ -756,7 +756,7 @@
   let
     val ps = merge_promises (promises1, promises2);
     val oracles = Oracles.merge (oracles1, oracles2);
-    val thms = Proofterm.merge_thms (thms1, thms2);
+    val thms = Proofterm.union_thms (thms1, thms2);
     val prf =
       (case ! Proofterm.proofs of
         2 => f prf1 prf2
@@ -976,7 +976,7 @@
 local
 
 fun union_digest (oracles1, thms1) (oracles2, thms2) =
-  (Oracles.merge (oracles1, oracles2), Proofterm.merge_thms (thms1, thms2));
+  (Oracles.merge (oracles1, oracles2), Proofterm.union_thms (thms1, thms2));
 
 fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) =
   (oracles, thms);