tuned;

--- a/src/Pure/proofterm.ML	Tue Apr 18 18:04:27 2023 +0200
+++ b/src/Pure/proofterm.ML	Tue Apr 18 18:27:22 2023 +0200
@@ -53,7 +53,9 @@
     proof_body list -> 'a -> 'a
   val oracle_ord: oracle ord
   val thm_ord: thm ord
+  val union_oracles: oracle Ord_List.T -> oracle Ord_List.T -> oracle Ord_List.T
   val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
+  val union_thms: thm Ord_List.T -> thm Ord_List.T -> thm Ord_List.T
   val unions_thms: thm Ord_List.T list -> thm Ord_List.T
   val no_proof_body: proof -> proof_body
   val no_thm_names: proof -> proof
@@ -316,7 +318,10 @@
 
 (* proof body *)
 
+val union_oracles = Ord_List.union oracle_ord;
 val unions_oracles = Ord_List.unions oracle_ord;
+
+val union_thms = Ord_List.union thm_ord;
 val unions_thms = Ord_List.unions thm_ord;
 
 fun no_proof_body proof = PBody {oracles = [], thms = [], proof = proof};

--- a/src/Pure/thm.ML	Tue Apr 18 18:04:27 2023 +0200
+++ b/src/Pure/thm.ML	Tue Apr 18 18:27:22 2023 +0200
@@ -777,8 +777,8 @@
     (Deriv {promises = ps2, body = PBody {oracles = oracles2, thms = thms2, proof = prf2}}) =
   let
     val ps = Ord_List.union promise_ord ps1 ps2;
-    val oracles = Proofterm.unions_oracles [oracles1, oracles2];
-    val thms = Proofterm.unions_thms [thms1, thms2];
+    val oracles = Proofterm.union_oracles oracles1 oracles2;
+    val thms = Proofterm.union_thms thms1 thms2;
     val prf =
       (case ! Proofterm.proofs of
         2 => f prf1 prf2
@@ -995,7 +995,7 @@
 local
 
 fun union_digest (oracles1, thms1) (oracles2, thms2) =
-  (Proofterm.unions_oracles [oracles1, oracles2], Proofterm.unions_thms [thms1, thms2]);
+  (Proofterm.union_oracles oracles1 oracles2, Proofterm.union_thms thms1 thms2);
 
 fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) =
   (oracles, thms);