diff -r 1a20fd9cf281 -r eb4ddd18d635 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Mon Apr 25 16:09:26 2016 +0200
@@ -60,12 +60,12 @@
 by(metis while_option_stop2)
 
 theorem while_option_rule:
-assumes step: "!!s. P s ==> b s ==> P (c s)"
-and result: "while_option b c s = Some t"
-and init: "P s"
-shows "P t"
+  assumes step: "!!s. P s ==> b s ==> P (c s)"
+    and result: "while_option b c s = Some t"
+    and init: "P s"
+  shows "P t"
 proof -
-  def k == "LEAST k. ~ b ((c ^^ k) s)"
+  define k where "k = (LEAST k. ~ b ((c ^^ k) s))"
   from assms have t: "t = (c ^^ k) s"
     by (simp add: while_option_def k_def split: if_splits)    
   have 1: "ALL i<k. b ((c ^^ i) s)"