diff -r 1b0f4071946c -r 9d5671f61b31 src/HOL/Import/Generate-HOL/GenHOL4Base.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Tue Jul 10 09:23:11 2007 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Tue Jul 10 09:23:12 2007 +0200
@@ -208,7 +208,7 @@
 import_theory divides;
 
 const_maps
-    divides > "Divides.dvd" :: "[nat,nat]=>bool";
+  divides > Divides.times_class.dvd :: "[nat,nat]=>bool";
 
 end_import;