# HG changeset patch
# User haftmann
# Date 1194647070 -3600
# Node ID 98b6b7f64e49930f85f8e57b3a65cf2cc8bad580
# Parent  05c2ae18cc5178c98f77dfbfaa9adda445fada7b
explicit message for failed autoquickcheck

diff -r 05c2ae18cc51 -r 98b6b7f64e49 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Nov 09 19:37:35 2007 +0100
+++ b/src/Pure/codegen.ML	Fri Nov 09 23:24:30 2007 +0100
@@ -995,8 +995,9 @@
     fun test state =
       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 as SOME _) => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
+            (try ((test_goal true (params, []) 1 assms)))) state of
+          SOME NONE => (Output.priority "Cannot auto quickcheck."; state)
+        | SOME (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 counterexamples found."; state)
       end;