src/HOL/Typedef.thy

--- a/src/HOL/Typedef.thy	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/Typedef.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -123,7 +123,7 @@
 text {* This class is just a workaround for classes without parameters;
   it shall disappear as soon as possible. *}
 
-class itself = type + 
+class itself = 
   fixes itself :: "'a itself"
 
 setup {*