# HG changeset patch
# User wenzelm
# Date 1703256190 -3600
# Node ID 56b604882d0b8e0cfb93ae84d603449407c9b0d9
# Parent  40cabd57aac34d9f3ceba053a3f0171fc8f5ad61
more thorough treatment of zproof vs. proof: avoid accidental storage of large structures;

diff -r 40cabd57aac3 -r 56b604882d0b src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Dec 22 14:55:55 2023 +0100
+++ b/src/Pure/proofterm.ML	Fri Dec 22 15:43:10 2023 +0100
@@ -255,8 +255,8 @@
 fun map_proof_of f (PBody {oracles, thms, zboxes, zproof, proof}) =
   PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = f proof};
 
-fun no_proofs (PBody {oracles, thms, zboxes, ...}) =
-  PBody {oracles = oracles, thms = thms, zboxes = zboxes, proof = MinProof, zproof = ZDummy};
+fun no_proof (PBody {oracles, thms, zboxes, zproof, ...}) =
+  PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = MinProof};
 
 fun thm_header serial pos theory_name name prop types : thm_header =
   {serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types};
@@ -2122,7 +2122,7 @@
 
 fun prune_body body =
   if Options.default_bool "prune_proofs"
-  then Future.map no_proofs body
+  then Future.map no_proof body
   else body;
 
 fun export_enabled () = Options.default_bool "export_proofs";
@@ -2217,7 +2217,7 @@
         val postproc = map_proof_of (unconstrainT #> named ? rew_proof thy);
         val body1 =
           {oracles = #oracles body0, thms = #thms body0,
-            zboxes = zboxes1, zproof = zproof1, proof = proof1};
+            zboxes = [], zproof = ZDummy, proof = proof1};
       in (i, fulfill_proof_future thy promises postproc (Future.value (PBody body1))) end;
 
     val (i, body') =
@@ -2234,9 +2234,10 @@
             else new_prf ()
         | _ => new_prf ());
 
+    val exp_proof = Future.map proof_of body';
     val open_proof = not named ? rew_proof thy;
+    fun export_body () = Future.join exp_proof |> open_proof |> export_proof thy i prop1;
 
-    fun export_body () = join_proof body' |> open_proof |> export_proof thy i prop1;
     val export =
       if export_enabled () then
         Lazy.lazy (fn () =>