src/Pure/Proof/extraction.ML

     val body =
       PBody
        {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;