--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Nov 30 09:21:11 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Nov 30 09:21:15 2011 +0100
@@ -153,6 +153,10 @@
fun test_card_size test_fun (card, size) =
(* FIXME: why decrement size by one? *)
let
+ val _ =
+ Quickcheck.message ctxt ("[Quickcheck-exhaustive] Test " ^
+ (if size = 0 then "" else "data size: " ^ string_of_int (size - 1) ^ " and ") ^
+ "cardinality: " ^ string_of_int card)
val (ts, timing) =
cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
(fn () => fst (test_fun [card, size - 1]))