src/Pure/Proof/extraction.ML

--- a/src/Pure/Proof/extraction.ML	Tue Apr 11 13:23:46 2023 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Apr 11 15:03:02 2023 +0200
@@ -182,7 +182,7 @@
           | _ => I);
     val body =
       PBody
-       {oracles = Ord_List.make Proofterm.oracle_ord oracles,
+       {oracles = Oracles.make oracles,
         thms = Ord_List.make Proofterm.thm_ord thms,
         proof = prf};
   in Proofterm.thm_body body end;