author | bulwahn |
Fri, 09 Dec 2011 12:21:01 +0100 | |
changeset 45792 | 4096351375cc |
parent 45791 | d985ec974815 |
child 45793 | 331ebffe0593 |
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri Dec 09 11:31:13 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri Dec 09 12:21:01 2011 +0100 @@ -113,6 +113,7 @@ !current_result) | SOME test_fun => let + val _ = Quickcheck.message ctxt ("Testing conjecture with with Quickcheck-" ^ name ^ "..."); val (response, exec_time) = cpu_time "quickcheck execution" (fn () => with_size test_fun genuine_only 1) val _ = Quickcheck.add_response names eval_terms response current_result