src/HOL/Library/Kleene_Algebras.thy

--- a/src/HOL/Library/Kleene_Algebras.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/src/HOL/Library/Kleene_Algebras.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -9,7 +9,7 @@
 
 text {* A type class of kleene algebras *}
 
-class star = 
+class star = type +
   fixes star :: "'a \<Rightarrow> 'a"
 
 class idem_add = ab_semigroup_add +