diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -36,7 +36,7 @@
   done
 
 definition
-  while :: "('a => bool) => ('a => 'a) => 'a => 'a"
+  while :: "('a => bool) => ('a => 'a) => 'a => 'a" where
   "while b c s = while_aux (b, c, s)"
 
 lemma while_aux_unfold: