src/HOL/Library/While_Combinator.thy

--- a/src/HOL/Library/While_Combinator.thy	Sun Nov 04 18:38:18 2012 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Sun Nov 04 18:41:27 2012 +0100
@@ -83,7 +83,7 @@
 definition while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
 where "while b c s = the (while_option b c s)"
 
-lemma while_unfold:
+lemma while_unfold [code]:
   "while b c s = (if b s then while b c (c s) else s)"
 unfolding while_def by (subst while_option_unfold) simp