# HG changeset patch
# User wenzelm
# Date 1703249583 -3600
# Node ID 8e0c80a9beb6af3378615b437bba5660df7ca59d
# Parent  d300a8f02b84df3de992367feaa2ffc770ebc433
observe option "prune_proofs";

diff -r d300a8f02b84 -r 8e0c80a9beb6 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Dec 21 21:35:54 2023 +0100
+++ b/src/Pure/thm.ML	Fri Dec 22 13:53:03 2023 +0100
@@ -2091,9 +2091,11 @@
       raise THM ("store_zproof: theorem may not use promises", 0, [thm]);
 
     val ((i, (zprop, zprf)), zproof') = ZTerm.thm_proof thy (name, pos) hyps prop zproof;
+    val (zboxes', zprf') =
+      if Options.default_bool "prune_proofs" then ([], ZDummy) else (zboxes, zprf);
     val thy' = thy
       |> (map_zproofs o Inttab.update)
-          (i, {thm_name = name, pos = pos, prop = zprop, zboxes = zboxes, zproof = zprf});
+          (i, {thm_name = name, pos = pos, prop = zprop, zboxes = zboxes', zproof = zprf'});
     val der' = make_deriv promises oracles thms [] zproof' proof;
   in (Thm (der', args), thy') end;