src/Tools/quickcheck.ML
changeset 30973 304ab57afa6e
parent 30824 bc6b24882834
child 30980 fe0855471964
     1.1 --- a/src/Tools/quickcheck.ML	Fri Apr 24 17:45:16 2009 +0200
     1.2 +++ b/src/Tools/quickcheck.ML	Fri Apr 24 17:45:17 2009 +0200
     1.3 @@ -15,19 +15,21 @@
     1.4  structure Quickcheck : QUICKCHECK =
     1.5  struct
     1.6  
     1.7 +open Quickcheck; (*c.f. Pure/Tools/ROOT.ML*)
     1.8 +
     1.9  (* quickcheck configuration -- default parameters, test generators *)
    1.10  
    1.11  datatype test_params = Test_Params of
    1.12    { size: int, iterations: int, default_type: typ option };
    1.13  
    1.14 -fun dest_test_params (Test_Params { size, iterations, default_type}) =
    1.15 +fun dest_test_params (Test_Params { size, iterations, default_type }) =
    1.16    ((size, iterations), default_type);
    1.17  fun mk_test_params ((size, iterations), default_type) =
    1.18    Test_Params { size = size, iterations = iterations, default_type = default_type };
    1.19  fun map_test_params f (Test_Params { size, iterations, default_type}) =
    1.20    mk_test_params (f ((size, iterations), default_type));
    1.21 -fun merge_test_params (Test_Params {size = size1, iterations = iterations1, default_type = default_type1},
    1.22 -  Test_Params {size = size2, iterations = iterations2, default_type = default_type2}) =
    1.23 +fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1 },
    1.24 +  Test_Params { size = size2, iterations = iterations2, default_type = default_type2 }) =
    1.25    mk_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
    1.26      case default_type1 of NONE => default_type2 | _ => default_type1);
    1.27  
    1.28 @@ -138,9 +140,6 @@
    1.29  
    1.30  (* automatic testing *)
    1.31  
    1.32 -val auto = ref false;
    1.33 -val auto_time_limit = ref 5000;
    1.34 -
    1.35  fun test_goal_auto int state =
    1.36    let
    1.37      val ctxt = Proof.context_of state;