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