src/HOL/Import/replay.ML
changeset 35842 7c170d39a808
parent 35742 eb8d2f668bfc
child 37778 87b5dfe00387
     1.1 --- a/src/HOL/Import/replay.ML	Fri Mar 19 00:46:08 2010 +0100
     1.2 +++ b/src/HOL/Import/replay.ML	Fri Mar 19 00:47:23 2010 +0100
     1.3 @@ -343,7 +343,8 @@
     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_global 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)
     1.9 +              (Binding.name t, map (rpair dummyS) vs, mx) c
    1.10          (Option.map (pairself Binding.name) repabs) (rtac (th_of thy th) 1) thy)
    1.11            | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
    1.12              add_hol4_type_mapping thyname tycname true fulltyname thy