1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 18 22:39:35 2012 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 18 22:40:25 2012 +0200
     1.3 @@ -242,6 +242,7 @@
     1.4          o Pretty.mark Isabelle_Markup.hilite
     1.5        else
     1.6          print o Pretty.string_of
     1.7 +    val pprint_a = pprint Output.urgent_message
     1.8      fun pprint_n f = () |> mode = Normal ? pprint Output.urgent_message o f
     1.9      fun pprint_v f = () |> verbose ? pprint Output.urgent_message o f
    1.10      fun pprint_d f = () |> debug ? pprint tracing o f
    1.11 @@ -670,7 +671,7 @@
    1.12            codatatypes_ok
    1.13          fun assms_prop () = Logic.mk_conjunction_list (neg_t :: assm_ts)
    1.14        in
    1.15 -        (pprint_n (fn () => Pretty.chunks
    1.16 +        (pprint_a (Pretty.chunks
    1.17               [Pretty.blk (0,
    1.18                    (pstrs ((if mode = Auto_Try then "Auto " else "") ^
    1.19                            "Nitpick found a" ^