--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Dec 12 13:45:54 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Dec 12 17:22:48 2011 +0100
@@ -113,7 +113,7 @@
!current_result)
| SOME test_fun =>
let
- val _ = Quickcheck.message ctxt ("Testing conjecture with with Quickcheck-" ^ name ^ "...");
+ val _ = Quickcheck.message ctxt ("Testing conjecture 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