# HG changeset patch
# User wenzelm
# Date 1194559065 -3600
# Node ID 96202af17d2bf2f2365db798380511292f39ece3
# Parent  7399b2480be88514076e33e65170a35a66c2cb3e
oops -- avoid vacous goal message;
tuned messages;

diff -r 7399b2480be8 -r 96202af17d2b src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu Nov 08 22:36:46 2007 +0100
+++ b/src/Pure/codegen.ML	Thu Nov 08 22:57:45 2007 +0100
@@ -996,9 +996,9 @@
       let val _ = Output.priority "Auto quickcheck ..." in
         case try (TimeLimit.timeLimit (Time.fromMilliseconds (!auto_quickcheck_time_limit))
             (test_goal true (params, []) 1 assms)) state of
-          SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
+          SOME (cex as SOME _) => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
             Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state
-        | _ => (Output.priority "Auto quickcheck: no counterexample found"; state)
+        | _ => (Output.priority "Auto quickcheck: no counterexamples found."; state)
       end;
   in
     if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)