--- a/src/Pure/Proof/extraction.ML Tue Apr 11 15:03:02 2023 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Apr 11 20:32:04 2023 +0200
@@ -180,11 +180,7 @@
(fn Oracle (name, prop, _) => apfst (cons ((name, Position.none), SOME prop))
| PThm (header, thm_body) => apsnd (cons (Proofterm.make_thm header thm_body))
| _ => I);
- val body =
- PBody
- {oracles = Oracles.make oracles,
- thms = Ord_List.make Proofterm.thm_ord thms,
- proof = prf};
+ val body = PBody {oracles = Oracles.make oracles, thms = PThms.make thms, proof = prf};
in Proofterm.thm_body body end;