--- 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)