src/HOL/Import/replay.ML
changeset 31723 f5cafe803b55
parent 30346 90efbb8a8cb2
child 32960 69916a850301
     1.1 --- a/src/HOL/Import/replay.ML	Thu Jun 18 18:31:14 2009 -0700
     1.2 +++ b/src/HOL/Import/replay.ML	Fri Jun 19 17:23:21 2009 +0200
     1.3 @@ -329,7 +329,7 @@
     1.4  	and rp (ThmEntry (thyname', thmname', aborted, History history)) thy = rps history thy	    
     1.5  	  | rp (DeltaEntry ds) thy = fold delta ds thy
     1.6  	and delta (Specification (names, th)) thy = 
     1.7 -	    fst (SpecificationPackage.add_specification NONE names (thy,th_of thy th))
     1.8 +	    fst (Choice_Specification.add_specification NONE names (thy,th_of thy th))
     1.9  	  | delta (Hol_mapping (thyname, thmname, isaname)) thy = 
    1.10  	    add_hol4_mapping thyname thmname isaname thy
    1.11  	  | delta (Hol_pending (thyname, thmname, th)) thy = 
    1.12 @@ -344,7 +344,7 @@
    1.13  	  | delta (Hol_theorem (thyname, thmname, th)) thy =
    1.14  	    add_hol4_theorem thyname thmname ([], th_of thy th) thy
    1.15  	  | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy = 
    1.16 -	    snd (TypedefPackage.add_typedef false (Option.map Binding.name thmname) (Binding.name t, vs, mx) c
    1.17 +	    snd (Typedef.add_typedef false (Option.map Binding.name thmname) (Binding.name t, vs, mx) c
    1.18          (Option.map (pairself Binding.name) repabs) (rtac (th_of thy th) 1) thy)
    1.19  	  | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
    1.20  	    add_hol4_type_mapping thyname tycname true fulltyname thy