adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck

--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Mar 02 22:13:32 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Mar 02 22:13:33 2010 +0100
@@ -54,7 +54,7 @@
 
 (* quickcheck options *)
 (*val quickcheck_generator = "SML"*)
-val iterations = 100
+val iterations = 10
 val size = 5
 
 exception RANDOM;

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Mar 02 22:13:32 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Mar 02 22:13:33 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,18 +29,16 @@
 
 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 options = Options {
@@ -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;

--- a/src/HOL/ex/Predicate_Compile_Quickcheck.thy	Tue Mar 02 22:13:32 2010 +0100
+++ b/src/HOL/ex/Predicate_Compile_Quickcheck.thy	Tue Mar 02 22:13:33 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