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 =