# HG changeset patch
# User bulwahn
# Date 1290422092 -3600
# Node ID 3dfa41e897382b2ee5cb45c91975e20b236200d5
# Parent  03ce94672ee6b723442b7312885a43630925de28
adding option finite_types to quickcheck

diff -r 03ce94672ee6 -r 3dfa41e89738 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Mon Nov 22 11:34:50 2010 +0100
+++ b/src/Tools/quickcheck.ML	Mon Nov 22 11:34:52 2010 +0100
@@ -87,10 +87,12 @@
 val (report, setup_report) = Attrib.config_bool "quickcheck_report" (K true)
 val (quiet, setup_quiet) = Attrib.config_bool "quickcheck_quiet" (K false)
 val (timeout, setup_timeout) = Attrib.config_real "quickcheck_timeout" (K 30.0)
+val (finite_types, setup_finite_types) = Attrib.config_bool "quickcheck_finite_types" (K true)
 
 val setup_config =
   setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_quiet #> setup_timeout
-  
+    #> setup_finite_types
+
 datatype test_params = Test_Params of
   {default_type: typ list, expect : expectation};
 
@@ -392,6 +394,7 @@
   | parse_test_param ("report", [arg]) = Config.put_generic report (read_bool arg)
   | parse_test_param ("quiet", [arg]) = Config.put_generic quiet (read_bool arg)
   | parse_test_param ("timeout", [arg]) = Config.put_generic timeout (read_real arg)
+  | parse_test_param ("finite_types", [arg]) = Config.put_generic finite_types (read_bool arg)
   | parse_test_param (name, _) = error ("Unknown test parameter: " ^ name);
 
 fun parse_test_param_inst ("generator", [arg]) ((generator, insts), ctxt) =