# HG changeset patch
# User blanchet
# Date 1280572196 -7200
# Node ID 36f649db4a6c60134eb59a6ca614738886e7c34e
# Parent  fb5e5a42594811db2cf672e91020ef0e2a0290ff
clarify Nitpick's output in case of a potential counterexample

diff -r fb5e5a425948 -r 36f649db4a6c doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Sat Jul 31 01:23:51 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Sat Jul 31 12:29:56 2010 +0200
@@ -818,7 +818,7 @@
 \hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount]
 Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
 \hbox{}\qquad Empty assignment \\[2\smallskipamount]
-Nitpick could not find a better counterexample. \\[2\smallskipamount]
+Nitpick could not find a better counterexample. It checked 1 of 1 scope. \\[2\smallskipamount]
 Total time: 2274 ms.
 \postw
 
diff -r fb5e5a425948 -r 36f649db4a6c src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Jul 31 01:23:51 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Jul 31 12:29:56 2010 +0200
@@ -904,9 +904,13 @@
                     "")); if skipped > 0 then "unknown" else "none")
           else
             (print_m (fn () =>
-                 "Nitpick could not find a" ^
-                 (if max_genuine = 1 then " better " ^ das_wort_model ^ "."
-                  else "ny better " ^ das_wort_model ^ "s.")); "potential")
+                 excipit ("could not find a" ^
+                          (if max_genuine = 1 then
+                             " better " ^ das_wort_model ^ "."
+                           else
+                             "ny better " ^ das_wort_model ^ "s.") ^
+                          " It checked"));
+             "potential")
         else if found_really_genuine then
           "genuine"
         else