# 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 ()