src/Pure/global_theory.ML
changeset 65458 cf504b7a7aa7
parent 62170 b61c55e4b4b9
child 67662 50db601cba27
--- a/src/Pure/global_theory.ML	Mon Apr 10 16:43:12 2017 +0200
+++ b/src/Pure/global_theory.ML	Mon Apr 10 21:05:31 2017 +0200
@@ -80,7 +80,7 @@
       fold (fn thy' => Symtab.update (Context.theory_name thy', thy'))
         (Theory.nodes_of thy) Symtab.empty;
     fun transfer th =
-      Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_name_of_thm th))) th;
+      Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_name th))) th;
   in transfer end;
 
 fun all_thms_of thy verbose =