--- 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