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