--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Dec 03 08:40:47 2010 +0100
@@ -22,7 +22,7 @@
val tracing : bool Unsynchronized.ref;
val quiet : bool Unsynchronized.ref;
val quickcheck_compile_term : Predicate_Compile_Aux.compilation -> bool -> bool -> int ->
- Proof.context -> term -> int -> term list option * (bool list * bool);
+ Proof.context -> term -> int -> term list option * Quickcheck.report option;
(* val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
val nrandom : int Unsynchronized.ref;
val debug : bool Unsynchronized.ref;
@@ -344,9 +344,8 @@
fun compile_term' compilation options depth ctxt t =
let
val c = compile_term compilation 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, NONE)
end
fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening depth =