src/HOL/Import/replay.ML
changeset 30346 90efbb8a8cb2
parent 29585 c23295521af5
child 31723 f5cafe803b55
     1.1 --- a/src/HOL/Import/replay.ML	Sat Mar 07 22:17:25 2009 +0100
     1.2 +++ b/src/HOL/Import/replay.ML	Sat Mar 07 23:30:58 2009 +0100
     1.3 @@ -334,7 +334,7 @@
     1.4  	    add_hol4_mapping thyname thmname isaname thy
     1.5  	  | delta (Hol_pending (thyname, thmname, th)) thy = 
     1.6  	    add_hol4_pending thyname thmname ([], th_of thy th) thy
     1.7 -	  | delta (Consts cs) thy = Sign.add_consts_i cs thy
     1.8 +	  | delta (Consts cs) thy = Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) cs) thy
     1.9  	  | delta (Hol_const_mapping (thyname, constname, fullcname)) thy = 
    1.10  	    add_hol4_const_mapping thyname constname true fullcname thy
    1.11  	  | delta (Hol_move (fullname, moved_thmname)) thy = 
    1.12 @@ -343,8 +343,9 @@
    1.13  	    snd (PureThy.add_defs false [((Binding.name thmname, eq), [])] thy)
    1.14  	  | delta (Hol_theorem (thyname, thmname, th)) thy =
    1.15  	    add_hol4_theorem thyname thmname ([], th_of thy th) thy
    1.16 -	  | delta (Typedef (thmname, typ, c, repabs, th)) thy = 
    1.17 -	    snd (TypedefPackage.add_typedef false thmname typ c repabs (rtac (th_of thy th) 1) thy)
    1.18 +	  | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy = 
    1.19 +	    snd (TypedefPackage.add_typedef false (Option.map Binding.name thmname) (Binding.name t, vs, mx) c
    1.20 +        (Option.map (pairself Binding.name) repabs) (rtac (th_of thy th) 1) thy)
    1.21  	  | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
    1.22  	    add_hol4_type_mapping thyname tycname true fulltyname thy
    1.23  	  | delta (Indexed_theorem (i, th)) thy =