--- a/src/HOL/Tools/quickcheck_generators.ML Thu Aug 19 11:19:24 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Thu Aug 19 12:11:57 2010 +0200
@@ -351,11 +351,11 @@
@{term "Pair :: term list option * (bool list * bool) => Random.seed => (term list option * (bool list * bool)) * Random.seed"};
fun mk_assms_report i =
HOLogic.mk_prod (@{term "None :: term list option"},
- HOLogic.mk_prod (HOLogic.mk_list @{typ "bool"}
- (replicate i @{term "True"} @ replicate (length assms - i) @{term "False"}),
- @{term "False"}))
+ HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT
+ (replicate i @{term True} @ replicate (length assms - i) @{term False}),
+ @{term False}))
fun mk_concl_report b =
- HOLogic.mk_prod (HOLogic.mk_list @{typ "bool"} (replicate (length assms) @{term "True"}),
+ HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT (replicate (length assms) @{term True}),
if b then @{term True} else @{term False})
val If =
@{term "If :: bool => term list option * (bool list * bool) => term list option * (bool list * bool) => term list option * (bool list * bool)"}