src/HOL/Import/replay.ML
changeset 39557 fe5722fce758
parent 37778 87b5dfe00387
child 41164 6854e9a40edc
     1.1 --- a/src/HOL/Import/replay.ML	Mon Sep 20 15:29:53 2010 +0200
     1.2 +++ b/src/HOL/Import/replay.ML	Mon Sep 20 16:05:25 2010 +0200
     1.3 @@ -339,7 +339,7 @@
     1.4            | delta (Hol_move (fullname, moved_thmname)) thy = 
     1.5              add_hol4_move fullname moved_thmname thy
     1.6            | delta (Defs (thmname, eq)) thy =
     1.7 -            snd (PureThy.add_defs false [((Binding.name thmname, eq), [])] thy)
     1.8 +            snd (Global_Theory.add_defs false [((Binding.name thmname, eq), [])] thy)
     1.9            | delta (Hol_theorem (thyname, thmname, th)) thy =
    1.10              add_hol4_theorem thyname thmname ([], th_of thy th) thy
    1.11            | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy =