src/HOL/Import/replay.ML
changeset 35742 eb8d2f668bfc
parent 33035 15eab423e573
child 35842 7c170d39a808
     1.1 --- a/src/HOL/Import/replay.ML	Sat Mar 13 14:42:16 2010 +0100
     1.2 +++ b/src/HOL/Import/replay.ML	Sat Mar 13 14:43:04 2010 +0100
     1.3 @@ -343,7 +343,7 @@
     1.4            | delta (Hol_theorem (thyname, thmname, th)) thy =
     1.5              add_hol4_theorem thyname thmname ([], th_of thy th) thy
     1.6            | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy = 
     1.7 -            snd (Typedef.add_typedef false (Option.map Binding.name thmname) (Binding.name t, vs, mx) c
     1.8 +            snd (Typedef.add_typedef_global false (Option.map Binding.name thmname) (Binding.name t, vs, mx) c
     1.9          (Option.map (pairself Binding.name) repabs) (rtac (th_of thy th) 1) thy)
    1.10            | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
    1.11              add_hol4_type_mapping thyname tycname true fulltyname thy