# HG changeset patch
# User wenzelm
# Date 1563962250 -7200
# Node ID 8473c1b32e2e1dade3be488a5bbcd4338efebf94
# Parent  64fdd75c1dea0341da0814cb207b2ea146eb997a
tuned;

diff -r 64fdd75c1dea -r 8473c1b32e2e src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Jul 24 11:54:08 2019 +0200
+++ b/src/Pure/proofterm.ML	Wed Jul 24 11:57:30 2019 +0200
@@ -1718,14 +1718,16 @@
         end;
 
     fun export i prf1 =
-     (if Options.default_bool "export_proofs" then
+     if Options.default_bool "export_proofs" then
         Export.export thy (Path.binding0 (Path.make ["proofs", string_of_int i]))
           (Buffer.chunks
             (YXML.buffer_body (Term_XML.Encode.term (term_of_proof prf1)) Buffer.empty))
       else ();
-      if Options.default_bool "prune_proofs" then MinProof else prf1);
 
-    fun publish i = clean_proof thy #> export i #> shrink_proof;
+    fun prune prf1 =
+      if Options.default_bool "prune_proofs" then MinProof else shrink_proof prf1;
+
+    fun publish i = clean_proof thy #> tap (export i) #> prune;
 
     fun new_prf () =
       let