# HG changeset patch
# User blanchet
# Date 1314018165 -7200
# Node ID d39aedffba083c22e1735196bf2d42857867eb7f
# Parent  20bd9f90accc37935e7b286b0a04e323dc6c2101
more precise warning

diff -r 20bd9f90accc -r d39aedffba08 src/HOL/Tools/Nitpick/nitpick.ML
--- 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