diff -r 38c63d4027c4 -r 960b866b1117 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Jul 12 14:18:56 2024 +0200
+++ b/src/Pure/Proof/extraction.ML	Sun Jul 14 15:16:08 2024 +0200
@@ -188,7 +188,7 @@
        {oracles = Ord_List.make Proofterm.oracle_ord oracles,
         thms = Ord_List.make Proofterm.thm_ord thms,
         zboxes = [],
-        zproof = ZDummy,
+        zproof = ZNop,
         proof = prf};
   in Proofterm.thm_body body end;