--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Tue Dec 20 13:04:46 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Tue Dec 20 14:43:41 2011 +0100
@@ -199,7 +199,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 ^ "...");
fun test genuine_only enum = case get_first (test_card_size test_fun genuine_only) enum of
SOME ((card, _), (true, ts)) =>
Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME (true, ts)) current_result