# 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