# HG changeset patch
# User bulwahn
# Date 1267605226 -3600
# Node ID 67879e5d695ce44da5fe05f33e7a3595901a1d41
# Parent  94170181a842f21de0eac1942744cd9b363b7d5f# Parent  00f3bbadbb2dd616d8e73742cff765d0a603970f
merged

diff -r 00f3bbadbb2d -r 67879e5d695c src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Mar 03 08:43:48 2010 +0100
+++ b/src/HOL/IsaMakefile	Wed Mar 03 09:33:46 2010 +0100
@@ -47,6 +47,7 @@
   HOL-MicroJava \
   HOL-Mirabelle \
   HOL-Modelcheck \
+  HOL-Mutabelle \
   HOL-NanoJava \
   HOL-Nitpick_Examples \
   HOL-Nominal-Examples \
diff -r 00f3bbadbb2d -r 67879e5d695c src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Mar 03 08:43:48 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Mar 03 09:33:46 2010 +0100
@@ -54,7 +54,7 @@
 
 (* quickcheck options *)
 (*val quickcheck_generator = "SML"*)
-val iterations = 100
+val iterations = 10
 val size = 5
 
 exception RANDOM;
diff -r 00f3bbadbb2d -r 67879e5d695c src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Mar 03 08:43:48 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Mar 03 09:33:46 2010 +0100
@@ -10,12 +10,10 @@
   val test_ref :
     ((unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option) Unsynchronized.ref
   val tracing : bool Unsynchronized.ref;
-  val quickcheck_compile_term : bool -> bool -> 
+  val quickcheck_compile_term : bool -> bool -> int ->
     Proof.context -> bool -> term -> int -> term list option * (bool list * bool);
 (*  val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
-  val quiet : bool Unsynchronized.ref;
   val nrandom : int Unsynchronized.ref;
-  val depth : int Unsynchronized.ref;
   val debug : bool Unsynchronized.ref;
   val function_flattening : bool Unsynchronized.ref;
   val no_higher_order_predicate : string list Unsynchronized.ref;
@@ -31,19 +29,17 @@
 
 val tracing = Unsynchronized.ref false;
 
-val target = "Quickcheck"
+val quiet = Unsynchronized.ref true;
 
-val quiet = Unsynchronized.ref false;
+val target = "Quickcheck"
 
 val nrandom = Unsynchronized.ref 2;
 
-val depth = Unsynchronized.ref 8;
+val debug = Unsynchronized.ref false;
 
-val debug = Unsynchronized.ref false;
 val function_flattening = Unsynchronized.ref true;
 
-
-val no_higher_order_predicate = Unsynchronized.ref [];
+val no_higher_order_predicate = Unsynchronized.ref ([] : string list);
 
 val options = Options {
   expected_modes = NONE,
@@ -231,21 +227,21 @@
 
 (* quickcheck interface functions *)
 
-fun compile_term' options ctxt report t =
+fun compile_term' options depth ctxt report t =
   let
     val c = compile_term options ctxt t
     val dummy_report = ([], false)
   in
-    fn size => (try_upto (!quiet) (c size (!nrandom)) (!depth), dummy_report)
+    fn size => (try_upto (!quiet) (c size (!nrandom)) depth, dummy_report)
   end
 
-fun quickcheck_compile_term function_flattening fail_safe_function_flattening ctxt t =
+fun quickcheck_compile_term function_flattening fail_safe_function_flattening depth =
   let
      val options =
        set_fail_safe_function_flattening fail_safe_function_flattening
          (set_function_flattening function_flattening (get_options ()))
   in
-    compile_term' options ctxt t
+    compile_term' options depth
   end
 
 end;
diff -r 00f3bbadbb2d -r 67879e5d695c src/HOL/ex/Predicate_Compile_Quickcheck.thy
--- a/src/HOL/ex/Predicate_Compile_Quickcheck.thy	Wed Mar 03 08:43:48 2010 +0100
+++ b/src/HOL/ex/Predicate_Compile_Quickcheck.thy	Wed Mar 03 09:33:46 2010 +0100
@@ -7,9 +7,9 @@
 uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
 begin
 
-setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term false true) *}
-setup {* Quickcheck.add_generator ("predicate_compile_ff_fs", Predicate_Compile_Quickcheck.quickcheck_compile_term true true) *}
-setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs", Predicate_Compile_Quickcheck.quickcheck_compile_term true false) *}
+setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term false true 8) *}
+setup {* Quickcheck.add_generator ("predicate_compile_ff_fs", Predicate_Compile_Quickcheck.quickcheck_compile_term true true 8) *}
+setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs", Predicate_Compile_Quickcheck.quickcheck_compile_term true false 8) *}
 
 (*
 datatype alphabet = a | b