src/Tools/quickcheck.ML
changeset 40894 3dfa41e89738
parent 40892 0850a2a16dce
child 40895 6e92ca8e981b
     1.1 --- a/src/Tools/quickcheck.ML	Mon Nov 22 11:34:50 2010 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Mon Nov 22 11:34:52 2010 +0100
     1.3 @@ -87,10 +87,12 @@
     1.4  val (report, setup_report) = Attrib.config_bool "quickcheck_report" (K true)
     1.5  val (quiet, setup_quiet) = Attrib.config_bool "quickcheck_quiet" (K false)
     1.6  val (timeout, setup_timeout) = Attrib.config_real "quickcheck_timeout" (K 30.0)
     1.7 +val (finite_types, setup_finite_types) = Attrib.config_bool "quickcheck_finite_types" (K true)
     1.8  
     1.9  val setup_config =
    1.10    setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_quiet #> setup_timeout
    1.11 -  
    1.12 +    #> setup_finite_types
    1.13 +
    1.14  datatype test_params = Test_Params of
    1.15    {default_type: typ list, expect : expectation};
    1.16  
    1.17 @@ -392,6 +394,7 @@
    1.18    | parse_test_param ("report", [arg]) = Config.put_generic report (read_bool arg)
    1.19    | parse_test_param ("quiet", [arg]) = Config.put_generic quiet (read_bool arg)
    1.20    | parse_test_param ("timeout", [arg]) = Config.put_generic timeout (read_real arg)
    1.21 +  | parse_test_param ("finite_types", [arg]) = Config.put_generic finite_types (read_bool arg)
    1.22    | parse_test_param (name, _) = error ("Unknown test parameter: " ^ name);
    1.23  
    1.24  fun parse_test_param_inst ("generator", [arg]) ((generator, insts), ctxt) =