# HG changeset patch
# User bulwahn
# Date 1323706968 -3600
# Node ID b85bb803bcf3ece3e95ad8b4325872cfcb56adc3
# Parent  53a697f5454ab3f08e613b6b4b4305cf8de84a9e
tuned quickcheck's response

diff -r 53a697f5454a -r b85bb803bcf3 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- 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