# HG changeset patch
# User bulwahn
# Date 1258054742 -3600
# Node ID e4aad90618ad5747b209ae7ea2a071876138c3af
# Parent  dd3ea99d5c763ad8b8ee35a8296656b769ee5496
adding the predicate compiler quickcheck to the ex/ROOT.ML; adopting this quickcheck to the latest changes

diff -r dd3ea99d5c76 -r e4aad90618ad src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Nov 12 20:38:59 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Nov 12 20:39:02 2009 +0100
@@ -23,6 +23,8 @@
 
 val options = Options {
   expected_modes = NONE,
+  proposed_modes = [],
+  proposed_names = [],
   show_steps = true,
   show_intermediate_results = true,
   show_proof_trace = false,
diff -r dd3ea99d5c76 -r e4aad90618ad src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu Nov 12 20:38:59 2009 +0100
+++ b/src/HOL/ex/ROOT.ML	Thu Nov 12 20:39:02 2009 +0100
@@ -13,7 +13,8 @@
   "Codegenerator_Pretty_Test",
   "NormalForm",
   "Predicate_Compile",
-  "Predicate_Compile_ex"
+  "Predicate_Compile_ex",
+  "Predicate_Compile_Quickcheck"
 ];
 
 use_thys [