--- 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);