--- 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
--- 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