src/HOL/Code_Setup.thy

--- a/src/HOL/Code_Setup.thy	Thu Jan 10 17:06:41 2008 +0100
+++ b/src/HOL/Code_Setup.thy	Thu Jan 10 19:09:21 2008 +0100
@@ -20,7 +20,9 @@
 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
 *}
 attach (test) {*
-fun gen_bool i = one_of [false, true];
+fun gen_bool i =
+  let val b = one_of [false, true]
+  in (b, fn () => term_of_bool b) end;
 *}
   "prop"  ("bool")
 attach (term_of) {*