# HG changeset patch
# User blanchet
# Date 1284466338 -7200
# Node ID 520ea38711e473e8aac4c584d91be7a22733c3f9
# Parent  cdf2c33414228de6c161ae38f35228cc3fcde415
tuning

diff -r cdf2c3341422 -r 520ea38711e4 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Sep 14 13:44:43 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Sep 14 14:12:18 2010 +0200
@@ -389,8 +389,8 @@
         print_m (K ("Warning: The problem involves directly or indirectly the \
                     \internal type " ^ quote @{type_name Datatype.node} ^
                     ". This type is very Nitpick-unfriendly, and its presence \
-                    \usually indicates either a failure in abstraction or a \
-                    \bug in Nitpick."))
+                    \usually indicates either a failure of abstraction or a \
+                    \quirk in Nitpick."))
       else
         ()
     val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
@@ -918,8 +918,8 @@
       in
         "Nitpick " ^ did_so_and_so ^
         (if is_some (!checked_problems) andalso total > 0 then
-           " " ^ string_of_int (Int.min (total - 1, unsat)) ^ " of " ^
-           string_of_int total ^ " scope" ^ plural_s total
+           " " ^ string_of_int unsat ^ " of " ^ string_of_int total ^ " scope"
+           ^ plural_s total
          else
            "") ^ "."
       end