src/Pure/codegen.ML
changeset 25358 7399b2480be8
parent 25309 30142fd3babf
child 25359 96202af17d2b
     1.1 --- a/src/Pure/codegen.ML	Thu Nov 08 22:19:43 2007 +0100
     1.2 +++ b/src/Pure/codegen.ML	Thu Nov 08 22:36:46 2007 +0100
     1.3 @@ -993,13 +993,12 @@
     1.4      val assms = map term_of (Assumption.assms_of ctxt)
     1.5      val params = get_test_params (Proof.theory_of state)
     1.6      fun test state =
     1.7 -      let val _ = Output.priority "Autoquickcheck..."
     1.8 -      in case try (TimeLimit.timeLimit (Time.fromMilliseconds (!auto_quickcheck_time_limit))
     1.9 -            (test_goal true (params, []) 1 assms)) state
    1.10 -       of NONE => (Output.priority "...no counterexample found"; state)
    1.11 -        | SOME NONE => (Output.priority "...no counterexample found"; state)
    1.12 -        | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
    1.13 +      let val _ = Output.priority "Auto quickcheck ..." in
    1.14 +        case try (TimeLimit.timeLimit (Time.fromMilliseconds (!auto_quickcheck_time_limit))
    1.15 +            (test_goal true (params, []) 1 assms)) state of
    1.16 +          SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
    1.17              Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state
    1.18 +        | _ => (Output.priority "Auto quickcheck: no counterexample found"; state)
    1.19        end;
    1.20    in
    1.21      if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)