Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
oops -- avoid vacous goal message;
authorwenzelm
Thu, 08 Nov 2007 22:57:45 +0100
changeset 25359 96202af17d2b
parent 25358 7399b2480be8
child 25360 b8251517f508
oops -- avoid vacous goal message; tuned messages;
src/Pure/codegen.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/codegen.ML	Thu Nov 08 22:36:46 2007 +0100
+++ b/src/Pure/codegen.ML	Thu Nov 08 22:57:45 2007 +0100
@@ -996,9 +996,9 @@
       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 "",
+          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 counterexample found"; state)
+        | _ => (Output.priority "Auto quickcheck: no counterexamples found."; state)
       end;
   in
     if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)
isabelle