src/HOL/Import/replay.ML
changeset 28662 64ab5bb68d4c
parent 27691 ce171cbd4b93
child 29585 c23295521af5
     1.1 --- a/src/HOL/Import/replay.ML	Wed Oct 22 14:15:43 2008 +0200
     1.2 +++ b/src/HOL/Import/replay.ML	Wed Oct 22 14:15:44 2008 +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 -	    snd (TypedefPackage.add_typedef_i false thmname typ c repabs (rtac (th_of thy th) 1) thy)
     1.8 +	    snd (TypedefPackage.add_typedef 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 =