--- a/src/HOL/Tools/Quickcheck/random_generators.ML Mon Dec 05 12:36:02 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Mon Dec 05 12:36:03 2011 +0100
@@ -372,8 +372,9 @@
val mk_parametric_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr
((mk_generator_expr,
- absdummy @{typ code_numeral} @{term "Pair None :: Random.seed => (bool * term list) option * Random.seed"}),
- @{typ "code_numeral => Random.seed => (bool * term list) option * Random.seed"})
+ absdummy @{typ bool} (absdummy @{typ code_numeral}
+ @{term "Pair None :: Random.seed => (bool * term list) option * Random.seed"})),
+ @{typ "bool => code_numeral => Random.seed => (bool * term list) option * Random.seed"})
val mk_parametric_reporting_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr
((mk_reporting_generator_expr,