registered directly executable version with the code generator

--- a/src/HOL/Library/While_Combinator.thy	Thu Jan 17 12:58:31 2002 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Thu Jan 17 15:06:36 2002 +0100
@@ -54,7 +54,7 @@
  The recursion equation for @{term while}: directly executable!
 *}
 
-theorem while_unfold:
+theorem while_unfold [code]:
     "while b c s = (if b s then while b c (c s) else s)"
   apply (unfold while_def)
   apply (rule while_aux_unfold [THEN trans])