src/HOL/Integ/Numeral.thy

--- a/src/HOL/Integ/Numeral.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/src/HOL/Integ/Numeral.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -42,7 +42,7 @@
   Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
   "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
 
-class number = -- {* for numeric types: nat, int, real, \dots *}
+class number = type + -- {* for numeric types: nat, int, real, \dots *}
   fixes number_of :: "int \<Rightarrow> 'a"
 
 syntax