Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Wed, 24 Jul 2019 11:57:30 +0200
changeset 70406 8473c1b32e2e
parent 70405 64fdd75c1dea
child 70407 e8558735961a
tuned;
src/Pure/proofterm.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle