--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Dec 05 12:35:58 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Dec 05 12:36:00 2011 +0100
@@ -284,7 +284,7 @@
val ctxt' = ctxt
|> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
|> Context.proof_map (exec false ml_code);
- val counterexample = get ctxt' ()
+ val counterexample = get ctxt' ()
in
if is_genuine counterexample then
(counterexample, !current_result)
@@ -431,7 +431,7 @@
let
fun dest_result (Quickcheck.Result r) = r
val opts =
- ((not (Config.get ctxt Quickcheck.potential), Config.get ctxt Quickcheck.quiet),
+ ((Config.get ctxt Quickcheck.genuine_only, Config.get ctxt Quickcheck.quiet),
Config.get ctxt Quickcheck.size)
val thy = Proof_Context.theory_of ctxt
val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Dec 05 12:35:58 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Dec 05 12:36:00 2011 +0100
@@ -69,7 +69,7 @@
fun test_term (name, compile) ctxt catch_code_errors (t, eval_terms) =
let
- val genuine_only = not (Config.get ctxt Quickcheck.potential)
+ val genuine_only = Config.get ctxt Quickcheck.genuine_only
val _ = check_test_term t
val names = Term.add_free_names t []
val current_size = Unsynchronized.ref 0
@@ -160,7 +160,7 @@
fun test_term_with_cardinality (name, compile) ctxt catch_code_errors ts =
let
- val genuine_only = not (Config.get ctxt Quickcheck.potential)
+ val genuine_only = Config.get ctxt Quickcheck.genuine_only
val thy = Proof_Context.theory_of ctxt
val (ts', eval_terms) = split_list ts
val _ = map check_test_term ts'
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Mon Dec 05 12:35:58 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Mon Dec 05 12:36:00 2011 +0100
@@ -350,7 +350,7 @@
(map_index I assms) concl_check
val check' = @{term "Quickcheck.catch_match :: term list option * bool list * bool =>
term list option * bool list * bool => term list option * bool list * bool"} $ check $
- (if Config.get ctxt Quickcheck.potential then
+ (if not (Config.get ctxt Quickcheck.genuine_only) then
HOLogic.mk_prod (@{term "Some :: term list => term list option"} $ terms, mk_concl_report false)
else
HOLogic.mk_prod (@{term "None :: term list option"}, mk_concl_report true))
--- a/src/Tools/quickcheck.ML Mon Dec 05 12:35:58 2011 +0100
+++ b/src/Tools/quickcheck.ML Mon Dec 05 12:36:00 2011 +0100
@@ -20,7 +20,7 @@
val no_assms : bool Config.T
val report : bool Config.T
val timing : bool Config.T
- val potential : bool Config.T
+ val genuine_only : bool Config.T
val quiet : bool Config.T
val timeout : real Config.T
val allow_function_inversion : bool Config.T;
@@ -174,7 +174,7 @@
val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
-val potential = Attrib.setup_config_bool @{binding quickcheck_potential} (K true)
+val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false)
val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false)
val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
val allow_function_inversion =
@@ -414,7 +414,7 @@
| parse_test_param ("no_assms", [arg]) = apsnd (Config.put_generic no_assms (read_bool arg))
| parse_test_param ("expect", [arg]) = apsnd (map_test_params ((apsnd o K) (read_expectation arg)))
| parse_test_param ("report", [arg]) = apsnd (Config.put_generic report (read_bool arg))
- | parse_test_param ("potential", [arg]) = apsnd (Config.put_generic potential (read_bool arg))
+ | parse_test_param ("genuine_only", [arg]) = apsnd (Config.put_generic genuine_only (read_bool arg))
| parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg))
| parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg))
| parse_test_param ("finite_types", [arg]) = apsnd (Config.put_generic finite_types (read_bool arg))