--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Aug 22 15:02:45 2011 +0200
@@ -928,8 +928,10 @@
forall (KK.is_problem_trivially_false o fst)
sound_problems then
print_n (fn () =>
- "Warning: The conjecture either trivially holds for the \
- \given scopes or lies outside Nitpick's supported \
+ "Warning: The conjecture " ^
+ (if falsify then "either trivially holds"
+ else "is either trivially unsatisfiable") ^
+ " for the given scopes or lies outside Nitpick's supported \
\fragment." ^
(if exists (not o KK.is_problem_trivially_false o fst)
unsound_problems then