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