src/HOL/Tools/Nitpick/nitpick.ML
changeset 42959 ee829022381d
parent 42486 01b03a124b81
child 43020 abb5d1f907e4
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue May 24 00:01:33 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue May 24 00:01:33 2011 +0200
     1.3 @@ -352,11 +352,12 @@
     1.4            pstrs ("The type" ^ plural_s_for_list pretties ^ " ") @
     1.5            pretty_serial_commas "and" pretties @
     1.6            pstrs (" " ^
     1.7 -          (if none_true monos then
     1.8 -             "passed the monotonicity test"
     1.9 -           else
    1.10 -             (if length pretties = 1 then "is" else "are") ^ " considered monotonic") ^
    1.11 -          ". " ^ extra))
    1.12 +                 (if none_true monos then
    1.13 +                    "passed the monotonicity test"
    1.14 +                  else
    1.15 +                    (if length pretties = 1 then "is" else "are") ^
    1.16 +                    " considered monotonic") ^
    1.17 +                 ". " ^ extra))
    1.18        end
    1.19      fun is_type_fundamentally_monotonic T =
    1.20        (is_datatype ctxt stds T andalso not (is_quot_type ctxt T) andalso