src/Pure/codegen.ML
changeset 25367 98b6b7f64e49
parent 25359 96202af17d2b
child 25376 87824cc5ff90
     1.1 --- a/src/Pure/codegen.ML	Fri Nov 09 19:37:35 2007 +0100
     1.2 +++ b/src/Pure/codegen.ML	Fri Nov 09 23:24:30 2007 +0100
     1.3 @@ -995,8 +995,9 @@
     1.4      fun test state =
     1.5        let val _ = Output.priority "Auto quickcheck ..." in
     1.6          case try (TimeLimit.timeLimit (Time.fromMilliseconds (!auto_quickcheck_time_limit))
     1.7 -            (test_goal true (params, []) 1 assms)) state of
     1.8 -          SOME (cex as SOME _) => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
     1.9 +            (try ((test_goal true (params, []) 1 assms)))) state of
    1.10 +          SOME NONE => (Output.priority "Cannot auto quickcheck."; state)
    1.11 +        | SOME (SOME (cex as SOME _)) => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
    1.12              Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state
    1.13          | _ => (Output.priority "Auto quickcheck: no counterexamples found."; state)
    1.14        end;