src/Pure/Proof/extraction.ML

--- a/src/Pure/Proof/extraction.ML	Thu Dec 14 12:21:09 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Thu Dec 14 17:33:45 2023 +0100
@@ -184,7 +184,7 @@
       PBody
        {oracles = Ord_List.make Proofterm.oracle_ord oracles,
         thms = Ord_List.make Proofterm.thm_ord thms,
-        zboxes = Proofterm.empty_zboxes,
+        zboxes = ZTerm.empty_zboxes,
         zproof = ZDummy,
         proof = prf};
   in Proofterm.thm_body body end;