src/HOL/SizeChange/Kleene_Algebras.thy

--- a/src/HOL/SizeChange/Kleene_Algebras.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/SizeChange/Kleene_Algebras.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -97,7 +97,7 @@
   and star4: "x * a \<le> x \<Longrightarrow> x * star a \<le> x"
 
 class kleene_by_complete_lattice = pre_kleene
-  + complete_lattice + recpower + star +
+  + complete_lattice + power + star +
   assumes star_cont: "a * star b * c = SUPR UNIV (\<lambda>n. a * b ^ n * c)"
 begin