diff -r 8df4c332cb1c -r 6a80fbc4e72c src/HOL/Library/Kleene_Algebra.thy
--- a/src/HOL/Library/Kleene_Algebra.thy	Tue Sep 13 13:17:52 2011 +0200
+++ b/src/HOL/Library/Kleene_Algebra.thy	Tue Sep 13 16:21:48 2011 +0200
@@ -377,19 +377,18 @@
   have [simp]: "1 \<le> star a"
     unfolding star_cont[of 1 a 1, simplified] 
     by (subst power_0[symmetric]) (rule le_SUPI [OF UNIV_I])
-  
-  show "1 + a * star a \<le> star a"
-    apply (rule plus_leI, simp)
-    apply (simp add:star_cont[of a a 1, simplified])
-    apply (simp add:star_cont[of 1 a 1, simplified])
-    apply (subst power_Suc[symmetric])
-    by (intro SUP_leI le_SUPI UNIV_I)
+
+  have "a * star a \<le> star a"
+    using star_cont[of a a 1] star_cont[of 1 a 1]
+    by (auto simp add: power_Suc[symmetric] simp del: power_Suc
+      intro: SUP_leI le_SUPI)
 
-  show "1 + star a * a \<le> star a" 
-    apply (rule plus_leI, simp)
-    apply (simp add:star_cont[of 1 a a, simplified])
-    apply (simp add:star_cont[of 1 a 1, simplified])
-    by (auto intro: SUP_leI le_SUPI simp add: power_Suc[symmetric] power_commutes simp del: power_Suc)
+  then show "1 + a * star a \<le> star a"
+    by simp
+
+  then show "1 + star a * a \<le> star a"
+    using star_cont[of a a 1] star_cont[of 1 a a]
+    by (simp add: power_commutes)
 
   show "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
   proof -