# HG changeset patch
# User bulwahn
# Date 1323084960 -3600
# Node ID e32dd098f57a6fe1f6162db73b8f99a87ce61e6a
# Parent  295658b28d3b1197bff53c939a9666cf043c6fcc
renaming potential flag to genuine_only flag with an inverse semantics

diff -r 295658b28d3b -r e32dd098f57a src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- 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
diff -r 295658b28d3b -r e32dd098f57a src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- 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'
diff -r 295658b28d3b -r e32dd098f57a src/HOL/Tools/Quickcheck/random_generators.ML
--- 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))
diff -r 295658b28d3b -r e32dd098f57a src/Tools/quickcheck.ML
--- 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))