changeset 77890 | 26d49c15bff0 |
parent 77889 | 5db014c36f42 |
child 78759 | 461e924cc825 |
--- a/src/Pure/proofterm.ML Thu Apr 20 11:57:34 2023 +0200 +++ b/src/Pure/proofterm.ML Thu Apr 20 12:23:41 2023 +0200 @@ -2137,7 +2137,7 @@ fun export_standard_enabled () = Options.default_bool "export_standard_proofs"; fun export_proof_boxes_required thy = - Context.theory_base_name thy = Context.PureN orelse + Context.theory_long_name thy = Context.PureN orelse (export_enabled () andalso not (export_standard_enabled ())); fun export_proof_boxes bodies =