# HG changeset patch
# User wenzelm
# Date 1194557806 -3600
# Node ID 7399b2480be88514076e33e65170a35a66c2cb3e
# Parent  6ea18fd1105834a6e61cb576610f71ad6b8aa8a0
tuned messages;
tuned;

diff -r 6ea18fd11058 -r 7399b2480be8 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu Nov 08 22:19:43 2007 +0100
+++ b/src/Pure/codegen.ML	Thu Nov 08 22:36:46 2007 +0100
@@ -993,13 +993,12 @@
     val assms = map term_of (Assumption.assms_of ctxt)
     val params = get_test_params (Proof.theory_of state)
     fun test state =
-      let val _ = Output.priority "Autoquickcheck..."
-      in case try (TimeLimit.timeLimit (Time.fromMilliseconds (!auto_quickcheck_time_limit))
-            (test_goal true (params, []) 1 assms)) state
-       of NONE => (Output.priority "...no counterexample found"; state)
-        | SOME NONE => (Output.priority "...no counterexample found"; state)
-        | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
+      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 "",
             Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state
+        | _ => (Output.priority "Auto quickcheck: no counterexample found"; state)
       end;
   in
     if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)