src/Pure/proofterm.ML
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 =