--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Feb 23 16:58:21 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Feb 25 09:28:01 2010 +0100
@@ -10,7 +10,8 @@
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 -> Proof.context -> term -> int -> term list option
+ val quickcheck_compile_term : bool -> bool ->
+ 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;
@@ -230,11 +231,12 @@
(* quickcheck interface functions *)
-fun compile_term' options ctxt t =
+fun compile_term' options 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))
+ fn size => (try_upto (!quiet) (c size (!nrandom)) (!depth), dummy_report)
end
fun quickcheck_compile_term function_flattening fail_safe_function_flattening ctxt t =