1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Feb 25 09:16:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Feb 25 10:08:44 2010 +0100
     1.3 @@ -342,7 +342,7 @@
     1.4        case triple_lookup (type_match thy) monos T of
     1.5          SOME (SOME b) => b
     1.6        | _ => is_type_always_monotonic T orelse
     1.7 -             formulas_monotonic hol_ctxt binarize T Plus def_ts nondef_ts core_t
     1.8 +             formulas_monotonic hol_ctxt binarize T (def_ts, nondef_ts, core_t)
     1.9      fun is_deep_datatype T =
    1.10        is_datatype thy stds T andalso
    1.11        (not standard orelse T = nat_T orelse is_word_type T orelse
    1.12 @@ -834,8 +834,8 @@
    1.13                          sound_problems then
    1.14                  print_m (fn () =>
    1.15                      "Warning: The conjecture either trivially holds for the \
    1.16 -                    \given scopes or (more likely) lies outside Nitpick's \
    1.17 -                    \supported fragment." ^
    1.18 +                    \given scopes or lies outside Nitpick's supported \
    1.19 +                    \fragment." ^
    1.20                      (if exists (not o KK.is_problem_trivially_false o fst)
    1.21                                 unsound_problems then
    1.22                         " Only potential counterexamples may be found."