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) {*

     2.1 --- a/src/HOL/Library/Efficient_Nat.thy	Thu Jan 10 17:06:41 2008 +0100
     2.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Jan 10 19:09:21 2008 +0100
     2.3 @@ -183,7 +183,9 @@
     2.4  val term_of_nat = HOLogic.mk_number HOLogic.natT;
     2.5  *}
     2.6  attach (test) {*
     2.7 -fun gen_nat i = random_range 0 i;
     2.8 +fun gen_nat i =
     2.9 +  let val n = random_range 0 i
    2.10 +  in (n, fn () => term_of_nat n) end;
    2.11  *}
    2.12  
    2.13  consts_code

     3.1 --- a/src/HOL/Library/Executable_Set.thy	Thu Jan 10 17:06:41 2008 +0100
     3.2 +++ b/src/HOL/Library/Executable_Set.thy	Thu Jan 10 19:09:21 2008 +0100
     3.3 @@ -250,9 +250,17 @@
     3.4        T --> Type ("set", [T]) --> Type ("set", [T])) $ f x $ term_of_set f T xs;
     3.5  *}
     3.6  attach (test) {*
     3.7 -fun gen_set' aG i j = frequency
     3.8 -  [(i, fn () => aG j :: gen_set' aG (i-1) j), (1, fn () => [])] ()
     3.9 -and gen_set aG i = gen_set' aG i i;
    3.10 +fun gen_set' aG aT i j = frequency
    3.11 +  [(i, fn () =>
    3.12 +      let
    3.13 +        val (x, t) = aG j;
    3.14 +        val (xs, ts) = gen_set' aG aT (i-1) j
    3.15 +      in
    3.16 +        (x :: xs, fn () => Const ("insert",
    3.17 +           aT --> Type ("set", [aT]) --> Type ("set", [aT])) $ t () $ ts ())
    3.18 +      end),
    3.19 +   (1, fn () => ([], fn () => Const ("{}", Type ("set", [aT]))))] ()
    3.20 +and gen_set aG aT i = gen_set' aG aT i i;
    3.21  *}
    3.22  
    3.23  

     4.1 --- a/src/HOL/List.thy	Thu Jan 10 17:06:41 2008 +0100
     4.2 +++ b/src/HOL/List.thy	Thu Jan 10 19:09:21 2008 +0100
     4.3 @@ -3100,16 +3100,23 @@
     4.4  fun term_of_list f T = HOLogic.mk_list T o map f;
     4.5  *}
     4.6  attach (test) {*
     4.7 -fun gen_list' aG i j = frequency
     4.8 -  [(i, fn () => aG j :: gen_list' aG (i-1) j), (1, fn () => [])] ()
     4.9 -and gen_list aG i = gen_list' aG i i;
    4.10 +fun gen_list' aG aT i j = frequency
    4.11 +  [(i, fn () =>
    4.12 +      let
    4.13 +        val (x, t) = aG j;
    4.14 +        val (xs, ts) = gen_list' aG aT (i-1) j
    4.15 +      in (x :: xs, fn () => HOLogic.cons_const aT $ t () $ ts ()) end),
    4.16 +   (1, fn () => ([], fn () => HOLogic.nil_const aT))] ()
    4.17 +and gen_list aG aT i = gen_list' aG aT i i;
    4.18  *}
    4.19    "char" ("string")
    4.20  attach (term_of) {*
    4.21  val term_of_char = HOLogic.mk_char o ord;
    4.22  *}
    4.23  attach (test) {*
    4.24 -fun gen_char i = chr (random_range (ord "a") (Int.min (ord "a" + i, ord "z")));
    4.25 +fun gen_char i =
    4.26 +  let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z"))
    4.27 +  in (chr j, fn () => HOLogic.mk_char j) end;
    4.28  *}
    4.29  
    4.30  consts_code "Cons" ("(_ ::/ _)")

     5.1 --- a/src/HOL/Numeral.thy	Thu Jan 10 17:06:41 2008 +0100
     5.2 +++ b/src/HOL/Numeral.thy	Thu Jan 10 19:09:21 2008 +0100
     5.3 @@ -644,7 +644,9 @@
     5.4  val term_of_int = HOLogic.mk_number HOLogic.intT;
     5.5  *}
     5.6  attach (test) {*
     5.7 -fun gen_int i = one_of [~1, 1] * random_range 0 i;
     5.8 +fun gen_int i =
     5.9 +  let val j = one_of [~1, 1] * random_range 0 i
    5.10 +  in (j, fn () => term_of_int j) end;
    5.11  *}
    5.12  
    5.13  setup {*

     6.1 --- a/src/HOL/Product_Type.thy	Thu Jan 10 17:06:41 2008 +0100
     6.2 +++ b/src/HOL/Product_Type.thy	Thu Jan 10 19:09:21 2008 +0100
     6.3 @@ -941,10 +941,14 @@
     6.4  types_code
     6.5    "*"     ("(_ */ _)")
     6.6  attach (term_of) {*
     6.7 -fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
     6.8 +fun term_of_id_42 aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y;
     6.9  *}
    6.10  attach (test) {*
    6.11 -fun gen_id_42 aG bG i = (aG i, bG i);
    6.12 +fun gen_id_42 aG aT bG bT i =
    6.13 +  let
    6.14 +    val (x, t) = aG i;
    6.15 +    val (y, u) = bG i
    6.16 +  in ((x, y), fn () => HOLogic.pair_const aT bT $ t () $ u ()) end;
    6.17  *}
    6.18  
    6.19  consts_code

     7.1 --- a/src/HOL/Real/Rational.thy	Thu Jan 10 17:06:41 2008 +0100
     7.2 +++ b/src/HOL/Real/Rational.thy	Thu Jan 10 19:09:21 2008 +0100
     7.3 @@ -713,7 +713,7 @@
     7.4      val rT = Type ("Rational.rat", [])
     7.5    in
     7.6      if q = 1 orelse p = 0 then HOLogic.mk_number rT p
     7.7 -    else Const ("HOL.inverse_class.divide", rT --> rT --> rT) $
     7.8 +    else @{term "op / \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat"} $
     7.9        HOLogic.mk_number rT p $ HOLogic.mk_number rT q
    7.10    end;
    7.11  *}
    7.12 @@ -725,9 +725,10 @@
    7.13      val g = Integer.gcd p q;
    7.14      val p' = p div g;
    7.15      val q' = q div g;
    7.16 +    val r = (if one_of [true, false] then p' else ~ p',
    7.17 +      if p' = 0 then 0 else q')
    7.18    in
    7.19 -    (if one_of [true, false] then p' else ~ p',
    7.20 -     if p' = 0 then 0 else q')
    7.21 +    (r, fn () => term_of_rat r)
    7.22    end;
    7.23  *}
    7.24  

     8.1 --- a/src/HOL/Real/RealDef.thy	Thu Jan 10 17:06:41 2008 +0100
     8.2 +++ b/src/HOL/Real/RealDef.thy	Thu Jan 10 19:09:21 2008 +0100
     8.3 @@ -1051,9 +1051,10 @@
     8.4      val g = Integer.gcd p q;
     8.5      val p' = p div g;
     8.6      val q' = q div g;
     8.7 +    val r = (if one_of [true, false] then p' else ~ p',
     8.8 +      if p' = 0 then 0 else q')
     8.9    in
    8.10 -    (if one_of [true, false] then p' else ~ p',
    8.11 -     if p' = 0 then 0 else q')
    8.12 +    (r, fn () => term_of_real r)
    8.13    end;
    8.14  *}
    8.15