--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Dec 05 12:36:05 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Dec 05 12:36:06 2011 +0100
@@ -14,7 +14,7 @@
-> (string * sort -> string * sort) option
val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
-> (typ option * (term * term list)) list list
- val mk_safe_if : term -> term * term * (bool -> term) -> term
+ val mk_safe_if : term -> term * term * (bool -> term) -> bool -> term
val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
type compile_generator =
Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
@@ -295,13 +295,13 @@
(* compilation of testing functions *)
-fun mk_safe_if genuine_only (cond, then_t, else_t) =
+fun mk_safe_if genuine_only (cond, then_t, else_t) genuine =
let
val T = @{typ "(bool * term list) option"}
val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T)
in
Const (@{const_name "Quickcheck.catch_match"}, T --> T --> T) $
- (if_t $ cond $ then_t $ else_t true) $
+ (if_t $ cond $ then_t $ else_t genuine) $
(if_t $ genuine_only $ Const (@{const_name "None"}, T) $ else_t false)
end