src/HOL/Import/replay.ML
changeset 24712 64ed05609568
parent 23139 aa899bce7c3b
child 27691 ce171cbd4b93
     1.1 --- a/src/HOL/Import/replay.ML	Tue Sep 25 15:34:35 2007 +0200
     1.2 +++ b/src/HOL/Import/replay.ML	Tue Sep 25 17:06:14 2007 +0200
     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 = Theory.add_consts_i cs thy
     1.8 +	  | delta (Consts cs) thy = Sign.add_consts_i 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 =