diff -r 5109e4b2a292 -r 686b7b14d041 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sat Dec 02 15:42:50 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Sat Dec 02 19:57:57 2023 +0100
@@ -184,6 +184,7 @@
       PBody
        {oracles = Ord_List.make Proofterm.oracle_ord oracles,
         thms = Ord_List.make Proofterm.thm_ord thms,
+        zboxes = Proofterm.empty_zboxes,
         proof = (prf, ZDummy)};
   in Proofterm.thm_body body end;