diff -r bfd9c0fd70b1 -r 753123c89d72 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/src/HOL/HOL.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -179,26 +179,26 @@
 
 subsubsection {* Generic algebraic operations *}
 
-class zero =
+class zero = type + 
   fixes zero :: "'a"  ("\<^loc>0")
 
-class one =
+class one = type +
   fixes one  :: "'a"  ("\<^loc>1")
 
 hide (open) const zero one
 
-class plus =
+class plus = type +
   fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>+" 65)
 
-class minus =
+class minus = type +
   fixes uminus :: "'a \<Rightarrow> 'a" 
     and minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>-" 65)
     and abs :: "'a \<Rightarrow> 'a"
 
-class times =
+class times = type +
   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>*" 70)
 
-class inverse = 
+class inverse = type +
   fixes inverse :: "'a \<Rightarrow> 'a"
     and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>'/" 70)