# HG changeset patch
# User blanchet
# Date 1334781625 -7200
# Node ID 366838a5e2352cb6fa0b04247c8ba84cf9885176
# Parent  55b42f9af99d48b7ba1b0b4082e2b6dfba774018
fixed Auto Nitpick's output

diff -r 55b42f9af99d -r 366838a5e235 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 18 22:39:35 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 18 22:40:25 2012 +0200
@@ -242,6 +242,7 @@
         o Pretty.mark Isabelle_Markup.hilite
       else
         print o Pretty.string_of
+    val pprint_a = pprint Output.urgent_message
     fun pprint_n f = () |> mode = Normal ? pprint Output.urgent_message o f
     fun pprint_v f = () |> verbose ? pprint Output.urgent_message o f
     fun pprint_d f = () |> debug ? pprint tracing o f
@@ -670,7 +671,7 @@
           codatatypes_ok
         fun assms_prop () = Logic.mk_conjunction_list (neg_t :: assm_ts)
       in
-        (pprint_n (fn () => Pretty.chunks
+        (pprint_a (Pretty.chunks
              [Pretty.blk (0,
                   (pstrs ((if mode = Auto_Try then "Auto " else "") ^
                           "Nitpick found a" ^