# HG changeset patch
# User wenzelm
# Date 1572619651 -3600
# Node ID a802d42c00bc06cddcfbb7f445b0013af6a04faa
# Parent  9dab828cbbc1282759d17e3bfc016eeab7e20a70
avoid redundant proof boxes for application sessions;

diff -r 9dab828cbbc1 -r a802d42c00bc src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Fri Nov 01 15:23:23 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Fri Nov 01 15:47:31 2019 +0100
@@ -291,7 +291,10 @@
           else MinProof;
         val (prop, SOME proof) =
           standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME proof0);
-        val _ = Proofterm.commit_proof proof;
+        val _ =
+          if Context.theory_name thy = Context.PureN orelse
+            (not export_standard_proofs andalso Proofterm.export_enabled ())
+          then Proofterm.commit_proof proof else ();
       in
         (prop, (deps, (boxes, proof))) |>
           let