--- 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