src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/src/HOL/Divides.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -12,7 +12,7 @@
 
 (*We use the same class for div and mod;
   moreover, dvd is defined whenever multiplication is*)
-class div =
+class div = type +
   fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
 begin