oops -- avoid vacous goal message;
authorwenzelm
Thu Nov 08 22:57:45 2007 +0100 (2007-11-08)
changeset 2535996202af17d2b
parent 25358 7399b2480be8
child 25360 b8251517f508
oops -- avoid vacous goal message;
tuned messages;
src/Pure/codegen.ML
     1.1 --- a/src/Pure/codegen.ML	Thu Nov 08 22:36:46 2007 +0100
     1.2 +++ b/src/Pure/codegen.ML	Thu Nov 08 22:57:45 2007 +0100
     1.3 @@ -996,9 +996,9 @@
     1.4        let val _ = Output.priority "Auto quickcheck ..." in
     1.5          case try (TimeLimit.timeLimit (Time.fromMilliseconds (!auto_quickcheck_time_limit))
     1.6              (test_goal true (params, []) 1 assms)) state of
     1.7 -          SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
     1.8 +          SOME (cex as SOME _) => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
     1.9              Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state
    1.10 -        | _ => (Output.priority "Auto quickcheck: no counterexample found"; state)
    1.11 +        | _ => (Output.priority "Auto quickcheck: no counterexamples found."; state)
    1.12        end;
    1.13    in
    1.14      if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)