--- a/src/HOL/Nat.thy Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/Nat.thy Wed Jan 21 23:40:23 2009 +0100
@@ -1515,7 +1515,7 @@
subsection {* size of a datatype value *}
-class size = type +
+class size =
fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded} *}
end