--- a/src/HOL/Nat.thy Mon Mar 19 19:28:27 2007 +0100
+++ b/src/HOL/Nat.thy Tue Mar 20 08:27:15 2007 +0100
@@ -106,7 +106,7 @@
text {* size of a datatype value *}
-class size =
+class size = type +
fixes size :: "'a \<Rightarrow> nat"
text {* @{typ nat} is a datatype *}
@@ -476,7 +476,7 @@
subsection {* Arithmetic operators *}
-class power =
+class power = type +
fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "\<^loc>^" 80)
text {* arithmetic operators @{text "+ -"} and @{text "*"} *}