src/Pure/Proof/extraction.ML

--- a/src/Pure/Proof/extraction.ML	Fri Dec 01 18:12:18 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Sat Dec 02 15:42:50 2023 +0100
@@ -184,7 +184,7 @@
       PBody
        {oracles = Ord_List.make Proofterm.oracle_ord oracles,
         thms = Ord_List.make Proofterm.thm_ord thms,
-        proof = prf};
+        proof = (prf, ZDummy)};
   in Proofterm.thm_body body end;