src/HOL/Int.thy

--- a/src/HOL/Int.thy	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/Int.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -599,7 +599,7 @@
   Bit1 :: "int \<Rightarrow> int" where
   [code del]: "Bit1 k = 1 + k + k"
 
-class number = type + -- {* for numeric types: nat, int, real, \dots *}
+class number = -- {* for numeric types: nat, int, real, \dots *}
   fixes number_of :: "int \<Rightarrow> 'a"
 
 use "Tools/numeral.ML"