# HG changeset patch
# User bulwahn
# Date 1324388621 -3600
# Node ID 28831430f230fcacfb88334d5c74e66a98845c49
# Parent  ddbe94f7242c13b7763d270fd43768469d7ee0ea
tuned

diff -r ddbe94f7242c -r 28831430f230 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- 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