diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Divides.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -11,7 +11,7 @@
 (*We use the same class for div and mod;
   moreover, dvd is defined whenever multiplication is*)
 axclass
-  div < term
+  div < type
 
 instance  nat :: div
 instance  nat :: plus_ac0 (add_commute,add_assoc,add_0)