src/HOL/Import/replay.ML

           | delta (Hol_const_mapping (thyname, constname, fullcname)) thy = 
             add_hol4_const_mapping thyname constname true fullcname thy
           | delta (Hol_move (fullname, moved_thmname)) thy = 
             add_hol4_move fullname moved_thmname thy
           | delta (Defs (thmname, eq)) thy =
-            snd (PureThy.add_defs false [((Binding.name thmname, eq), [])] thy)
+            snd (Global_Theory.add_defs false [((Binding.name thmname, eq), [])] thy)
           | delta (Hol_theorem (thyname, thmname, th)) thy =
             add_hol4_theorem thyname thmname ([], th_of thy th) thy
           | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy = 
             snd (Typedef.add_typedef_global false (Option.map Binding.name thmname)
               (Binding.name t, map (rpair dummyS) vs, mx) c