1.1 --- a/src/HOL/HOL.thy	Mon Mar 19 19:28:27 2007 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Mar 20 08:27:15 2007 +0100
     1.3 @@ -179,26 +179,26 @@
     1.4  
     1.5  subsubsection {* Generic algebraic operations *}
     1.6  
     1.7 -class zero =
     1.8 +class zero = type + 
     1.9    fixes zero :: "'a"  ("\<^loc>0")
    1.10  
    1.11 -class one =
    1.12 +class one = type +
    1.13    fixes one  :: "'a"  ("\<^loc>1")
    1.14  
    1.15  hide (open) const zero one
    1.16  
    1.17 -class plus =
    1.18 +class plus = type +
    1.19    fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>+" 65)
    1.20  
    1.21 -class minus =
    1.22 +class minus = type +
    1.23    fixes uminus :: "'a \<Rightarrow> 'a" 
    1.24      and minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>-" 65)
    1.25      and abs :: "'a \<Rightarrow> 'a"
    1.26  
    1.27 -class times =
    1.28 +class times = type +
    1.29    fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>*" 70)
    1.30  
    1.31 -class inverse = 
    1.32 +class inverse = type +
    1.33    fixes inverse :: "'a \<Rightarrow> 'a"
    1.34      and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>'/" 70)
    1.35