diff -r 08f3491c50bf -r 355a4cac5440 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Tue Sep 03 19:58:00 2013 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Tue Sep 03 22:04:23 2013 +0200
@@ -93,8 +93,9 @@
   next
     case (Suc k)
     hence "\<not> b ((c^^k) (c s))" by (auto simp: funpow_swap1)
-    then guess k by (rule exE[OF Suc.IH[of "c s"]])
-    with assms show ?case by (cases "b s") (auto simp: funpow_swap1 intro: exI[of _ "Suc k"] exI[of _ "0"])
+    from Suc.IH[OF this] obtain k where "\<not> b' ((c' ^^ k) (f (c s)))" ..
+    with assms show ?case
+      by (cases "b s") (auto simp: funpow_swap1 intro: exI[of _ "Suc k"] exI[of _ "0"])
   qed
 next
   fix k assume "\<not> b' ((c' ^^ k) (f s))"
@@ -107,8 +108,8 @@
     show ?case
     proof (cases "b s")
       case True
-      with assms(2) * have "\<not> b' ((c'^^k) (f (c s)))" by simp 
-      then guess k by (rule exE[OF Suc.IH[of "c s"]])
+      with assms(2) * have "\<not> b' ((c'^^k) (f (c s)))" by simp
+      from Suc.IH[OF this] obtain k where "\<not> b ((c ^^ k) (c s))" ..
       thus ?thesis by (auto simp: funpow_swap1 intro: exI[of _ "Suc k"])
     qed (auto intro: exI[of _ "0"])
   qed