src/Tools/quickcheck.ML

--- a/src/Tools/quickcheck.ML	Thu Jul 30 23:50:11 2009 +0200
+++ b/src/Tools/quickcheck.ML	Fri Jul 31 23:30:21 2009 +0200
@@ -11,6 +11,7 @@
   val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
     (string * term) list option
   val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
+  val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option
 end;
 
 structure Quickcheck : QUICKCHECK =
@@ -215,18 +216,21 @@
     |> (Data.map o apsnd o map_test_params) f
   end;
 
-fun quickcheck_cmd args i state =
+fun quickcheck args i state =
   let
-    val prf = Toplevel.proof_of state;
-    val thy = Toplevel.theory_of state;
-    val ctxt = Toplevel.context_of state;
+    val thy = Proof.theory_of state;
+    val ctxt = Proof.context_of state;
     val default_params = (dest_test_params o snd o Data.get) thy;
     val f = fold (parse_test_param_inst ctxt) args;
     val (((size, iterations), default_type), (generator_name, insts)) =
       f (default_params, (NONE, []));
-    val counterex = test_goal false generator_name size iterations
-      default_type insts i [] prf;
-  in (Pretty.writeln o pretty_counterex ctxt) counterex end;
+  in
+    test_goal false generator_name size iterations default_type insts i [] state
+  end;
+
+fun quickcheck_cmd args i state =
+  quickcheck args i (Toplevel.proof_of state)
+  |> Pretty.writeln o pretty_counterex (Toplevel.context_of state);
 
 local structure P = OuterParse and K = OuterKeyword in