src/Pure/Proof/extraction.ML

--- a/src/Pure/Proof/extraction.ML	Mon Dec 18 12:02:58 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Mon Dec 18 12:57:59 2023 +0100
@@ -184,7 +184,7 @@
       PBody
        {oracles = Ord_List.make Proofterm.oracle_ord oracles,
         thms = Ord_List.make Proofterm.thm_ord thms,
-        zboxes = ZTerm.empty_zboxes,
+        zboxes = [],
         zproof = ZDummy,
         proof = prf};
   in Proofterm.thm_body body end;