src/HOL/Import/replay.ML
changeset 24712 64ed05609568
parent 23139 aa899bce7c3b
child 27691 ce171cbd4b93
--- a/src/HOL/Import/replay.ML	Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Import/replay.ML	Tue Sep 25 17:06:14 2007 +0200
@@ -334,7 +334,7 @@
 	    add_hol4_mapping thyname thmname isaname thy
 	  | delta (Hol_pending (thyname, thmname, th)) thy = 
 	    add_hol4_pending thyname thmname ([], th_of thy th) thy
-	  | delta (Consts cs) thy = Theory.add_consts_i cs thy
+	  | delta (Consts cs) thy = Sign.add_consts_i cs thy
 	  | delta (Hol_const_mapping (thyname, constname, fullcname)) thy = 
 	    add_hol4_const_mapping thyname constname true fullcname thy
 	  | delta (Hol_move (fullname, moved_thmname)) thy =