src/HOL/Import/replay.ML
changeset 19349 36e537f89585
parent 19203 778507520684
child 21078 101aefd61aac
     1.1 --- a/src/HOL/Import/replay.ML	Thu Apr 06 16:12:57 2006 +0200
     1.2 +++ b/src/HOL/Import/replay.ML	Thu Apr 06 16:13:17 2006 +0200
     1.3 @@ -344,7 +344,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, typ, c, repabs, th)) thy = 
     1.7 -	    fst(TypedefPackage.add_typedef_i false thmname typ c repabs (rtac (th_of thy th) 1) thy)
     1.8 +	    snd (TypedefPackage.add_typedef_i false thmname typ c repabs (rtac (th_of thy th) 1) thy)
     1.9  	  | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
    1.10  	    add_hol4_type_mapping thyname tycname true fulltyname thy
    1.11  	  | delta (Indexed_theorem (i, th)) thy =