--- 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;