--- a/src/Tools/quickcheck.ML Fri Apr 24 17:45:16 2009 +0200
+++ b/src/Tools/quickcheck.ML Fri Apr 24 17:45:17 2009 +0200
@@ -15,19 +15,21 @@
structure Quickcheck : QUICKCHECK =
struct
+open Quickcheck; (*c.f. Pure/Tools/ROOT.ML*)
+
(* quickcheck configuration -- default parameters, test generators *)
datatype test_params = Test_Params of
{ size: int, iterations: int, default_type: typ option };
-fun dest_test_params (Test_Params { size, iterations, default_type}) =
+fun dest_test_params (Test_Params { size, iterations, default_type }) =
((size, iterations), default_type);
fun mk_test_params ((size, iterations), default_type) =
Test_Params { size = size, iterations = iterations, default_type = default_type };
fun map_test_params f (Test_Params { size, iterations, default_type}) =
mk_test_params (f ((size, iterations), default_type));
-fun merge_test_params (Test_Params {size = size1, iterations = iterations1, default_type = default_type1},
- Test_Params {size = size2, iterations = iterations2, default_type = default_type2}) =
+fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1 },
+ Test_Params { size = size2, iterations = iterations2, default_type = default_type2 }) =
mk_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
case default_type1 of NONE => default_type2 | _ => default_type1);
@@ -138,9 +140,6 @@
(* automatic testing *)
-val auto = ref false;
-val auto_time_limit = ref 5000;
-
fun test_goal_auto int state =
let
val ctxt = Proof.context_of state;