src/HOL/Import/replay.ML
changeset 27691 ce171cbd4b93
parent 24712 64ed05609568
child 28662 64ab5bb68d4c
     1.1 --- a/src/HOL/Import/replay.ML	Tue Jul 29 08:15:39 2008 +0200
     1.2 +++ b/src/HOL/Import/replay.ML	Tue Jul 29 08:15:40 2008 +0200
     1.3 @@ -340,7 +340,7 @@
     1.4  	  | delta (Hol_move (fullname, moved_thmname)) thy = 
     1.5  	    add_hol4_move fullname moved_thmname thy
     1.6  	  | delta (Defs (thmname, eq)) thy =
     1.7 -	    snd (PureThy.add_defs_i false [((thmname, eq), [])] thy)
     1.8 +	    snd (PureThy.add_defs false [((thmname, eq), [])] thy)
     1.9  	  | delta (Hol_theorem (thyname, thmname, th)) thy =
    1.10  	    add_hol4_theorem thyname thmname ([], th_of thy th) thy
    1.11  	  | delta (Typedef (thmname, typ, c, repabs, th)) thy =