fixed Auto Nitpick's output
authorblanchet
Wed, 18 Apr 2012 22:40:25 +0200
changeset 47559 366838a5e235
parent 47558 55b42f9af99d
child 47560 e30323bfc93c
fixed Auto Nitpick's output
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" ^