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