diff -r 8020249565fb -r 5976fe402824 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Sun Sep 13 16:50:12 2015 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Sun Sep 13 20:20:16 2015 +0200
@@ -157,7 +157,7 @@
     note b = this(1) and body = this(2) and inv = this(3)
     hence k': "f ((c ^^ k') s) = (c' ^^ k') (f s)" by auto
     ultimately show ?thesis unfolding Suc using b
-    proof (intro Least_equality[symmetric], goals)
+    proof (intro Least_equality[symmetric], goal_cases)
       case 1
       hence Test: "\<not> b' (f ((c ^^ Suc k') s))"
         by (auto simp: BodyCommute inv b)