proper theory_long_name;

--- a/src/Pure/global_theory.ML	Thu Apr 20 11:57:34 2023 +0200
+++ b/src/Pure/global_theory.ML	Thu Apr 20 12:23:41 2023 +0200
@@ -172,9 +172,9 @@
   let
     val theories =
       Symtab.build (Theory.nodes_of thy |> fold (fn thy' =>
-        Symtab.update (Context.theory_base_name thy', thy')));
+        Symtab.update (Context.theory_long_name thy', thy')));
     fun transfer th =
-      Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_base_name th))) th;
+      Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_long_name th))) th;
   in transfer end;
 
 fun all_thms_of thy verbose =

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