diff -r 3728dba101f1 -r bd3b60f9a343 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Sun Oct 01 12:07:57 2006 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Sun Oct 01 18:29:23 2006 +0200
@@ -37,7 +37,7 @@
 
 definition
   while :: "('a => bool) => ('a => 'a) => 'a => 'a"
-  "while b c s == while_aux (b, c, s)"
+  "while b c s = while_aux (b, c, s)"
 
 lemma while_aux_unfold:
   "while_aux (b, c, s) =