# HG changeset patch
# User wenzelm
# Date 1436191381 -7200
# Node ID 3a0aaf894e21c42fd57c34a419254580a6f57beb
# Parent  61be352b1f79924daedf93f0c18931404a953ad5
tuned message;

diff -r 61be352b1f79 -r 3a0aaf894e21 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Mon Jul 06 15:45:08 2015 +0200
+++ b/src/Tools/quickcheck.ML	Mon Jul 06 16:03:01 2015 +0200
@@ -340,7 +340,6 @@
   let
     val lthy = Proof.context_of state;
     val thy = Proof.theory_of state;
-    val _ = message lthy "Quickchecking..."
     fun strip (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = strip t
       | strip t = t;
     val {goal = st, ...} = Proof.raw_goal state;
@@ -390,8 +389,9 @@
         val header =
           Pretty.para
             (tool_name auto ^ " found a " ^
-              (if genuine then "counterexample:"
-               else "potentially spurious counterexample due to underspecified functions:") ^
+              (if genuine then "counterexample"
+               else "potentially spurious counterexample due to underspecified functions") ^
+              (if null cex then "." else ":") ^
               Config.get ctxt tag);
         fun pretty_cex (x, t) =
           Pretty.block [Pretty.str (x ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t];