diff -r 915da29bf5d9 -r 7e741e22d7fc src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Thu Jun 25 23:33:47 2015 +0200
@@ -157,14 +157,15 @@
     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])
-      case goal1
+    proof (intro Least_equality[symmetric], goals)
+      case 1
       hence Test: "\<not> b' (f ((c ^^ Suc k') s))"
         by (auto simp: BodyCommute inv b)
       have "P ((c ^^ Suc k') s)" by (auto simp: Invariant inv b)
       with Test show ?case by (auto simp: TestCommute)
     next
-      case goal2 thus ?case by (metis not_less_eq_eq)
+      case 2
+      thus ?case by (metis not_less_eq_eq)
     qed
   qed
   have "f ((c ^^ ?k) s) = (c' ^^ ?k') (f s)" unfolding *