# HG changeset patch # User bulwahn # Date 1285246218 -7200 # Node ID f398f66969cef077b027f1c48e9ce16b6cd024ec # Parent 8ad7fe9d6f0be0822bb01fb9bc4455c8a6dd3ab0 exporting the generic version instead of the context version in quickcheck diff -r 8ad7fe9d6f0b -r f398f66969ce src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Thu Sep 23 14:50:18 2010 +0200 +++ b/src/Tools/quickcheck.ML Thu Sep 23 14:50:18 2010 +0200 @@ -19,7 +19,7 @@ expect : expectation, report: bool, quiet : bool}; val test_params_of: Proof.context -> test_params val report : Proof.context -> bool - val set_reporting : bool -> Proof.context -> Proof.context + val set_reporting : bool -> Context.generic -> Context.generic val add_generator: string * (Proof.context -> term -> int -> term list option * (bool list * bool)) -> Context.generic -> Context.generic @@ -122,7 +122,7 @@ fun map_report f (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) = make_test_params ((size, iterations), ((default_type, no_assms), ((expect, f report), quiet))); -fun set_reporting report = Context.proof_map (Data.map (apsnd (map_report (K report)))) +fun set_reporting report = Data.map (apsnd (map_report (K report))) val add_generator = Data.map o apfst o AList.update (op =); @@ -204,7 +204,7 @@ fun test_term ctxt quiet generator_name size i t = ctxt - |> set_reporting false + |> Context.proof_map (set_reporting false) |> (fn ctxt' => fst (gen_test_term ctxt' quiet generator_name size i t)) exception WELLSORTED of string @@ -310,7 +310,7 @@ (snd o Data.get o Context.Proof) ctxt; val res = state - |> Proof.map_context (set_reporting false) + |> Proof.map_context (Context.proof_map (set_reporting false)) |> try (test_goal true NONE size iterations default_type no_assms [] 1); in case res of @@ -382,7 +382,7 @@ f (default_params, (NONE, [])); in state - |> Proof.map_context (set_reporting report) + |> Proof.map_context (Context.proof_map (set_reporting report)) |> test_goal quiet generator_name size iterations default_type no_assms insts i |> tap (fn (SOME x, _) => if expect = No_Counterexample then error ("quickcheck expected to find no counterexample but found one") else ()