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" ^