src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 45757 e32dd098f57a
parent 45756 295658b28d3b
child 45760 3b5a735897c3
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Dec 05 12:35:58 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Dec 05 12:36:00 2011 +0100
     1.3 @@ -284,7 +284,7 @@
     1.4                    val ctxt' = ctxt
     1.5                      |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
     1.6                      |> Context.proof_map (exec false ml_code);                 
     1.7 -                  val counterexample =  get ctxt' ()
     1.8 +                  val counterexample = get ctxt' ()
     1.9                  in
    1.10                    if is_genuine counterexample then
    1.11                      (counterexample, !current_result)
    1.12 @@ -431,7 +431,7 @@
    1.13    let
    1.14      fun dest_result (Quickcheck.Result r) = r 
    1.15      val opts =
    1.16 -      ((not (Config.get ctxt Quickcheck.potential), Config.get ctxt Quickcheck.quiet),
    1.17 +      ((Config.get ctxt Quickcheck.genuine_only, Config.get ctxt Quickcheck.quiet),
    1.18          Config.get ctxt Quickcheck.size)
    1.19      val thy = Proof_Context.theory_of ctxt
    1.20      val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t