src/Pure/global_theory.ML
changeset 77889 5db014c36f42
parent 74561 8e6c973003c8
child 77890 26d49c15bff0
--- a/src/Pure/global_theory.ML	Wed Apr 19 23:27:55 2023 +0200
+++ b/src/Pure/global_theory.ML	Thu Apr 20 11:57:34 2023 +0200
@@ -172,9 +172,9 @@
   let
     val theories =
       Symtab.build (Theory.nodes_of thy |> fold (fn thy' =>
-        Symtab.update (Context.theory_name thy', thy')));
+        Symtab.update (Context.theory_base_name thy', thy')));
     fun transfer th =
-      Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_name th))) th;
+      Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_base_name th))) th;
   in transfer end;
 
 fun all_thms_of thy verbose =