src/HOL/Tools/Quickcheck/quickcheck_common.ML

     case test_fun of
       NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
         !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
         val _ = Quickcheck.add_timing exec_time current_result
       in !current_result end