# HG changeset patch
# User blanchet
# Date 1265727949 -3600
# Node ID c1dac8ace020750f836a6ebd3117682a16e86d85
# Parent  cc19e2aef17e3fb127b427871cebce915f0ca9a6
make Quickcheck identify itself, so people don't submit bug reports to me thinking that it was Nitpick

diff -r cc19e2aef17e -r c1dac8ace020 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Fri Feb 05 14:27:21 2010 +0100
+++ b/src/Tools/quickcheck.ML	Tue Feb 09 16:05:49 2010 +0100
@@ -153,9 +153,9 @@
       |> ObjectLogic.atomize_term thy;
   in test_term ctxt quiet generator_name size iterations gi' end;
 
-fun pretty_counterex ctxt NONE = Pretty.str "No counterexamples found."
+fun pretty_counterex ctxt NONE = Pretty.str "Quickcheck found no counterexample."
   | pretty_counterex ctxt (SOME cex) =
-      Pretty.chunks (Pretty.str "Counterexample found:\n" ::
+      Pretty.chunks (Pretty.str "Quickcheck found a counterexample:\n" ::
         map (fn (s, t) =>
           Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);