src/HOL/Code_Setup.thy
changeset 25885 6fbc3f54f819
parent 25866 263aaf988d44
child 25916 d957d9982241
     1.1 --- a/src/HOL/Code_Setup.thy	Thu Jan 10 17:06:41 2008 +0100
     1.2 +++ b/src/HOL/Code_Setup.thy	Thu Jan 10 19:09:21 2008 +0100
     1.3 @@ -20,7 +20,9 @@
     1.4  fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
     1.5  *}
     1.6  attach (test) {*
     1.7 -fun gen_bool i = one_of [false, true];
     1.8 +fun gen_bool i =
     1.9 +  let val b = one_of [false, true]
    1.10 +  in (b, fn () => term_of_bool b) end;
    1.11  *}
    1.12    "prop"  ("bool")
    1.13  attach (term_of) {*