--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Oct 25 20:24:13 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Oct 25 21:06:56 2010 +0200
@@ -216,7 +216,7 @@
o Pretty.chunks o cons (Pretty.str "") o single
o Pretty.mark Markup.hilite
else
- (fn s => (priority s; if debug then tracing s else ()))
+ (fn s => (Output.urgent_message s; if debug then tracing s else ()))
o Pretty.string_of
fun pprint_m f = () |> not auto ? pprint o f
fun pprint_v f = () |> verbose ? pprint o f
@@ -989,7 +989,7 @@
raise Interrupt
else
if passed_deadline deadline then
- (priority "Nitpick ran out of time."; ("unknown", state))
+ (Output.urgent_message "Nitpick ran out of time."; ("unknown", state))
else
error "Nitpick was interrupted."
@@ -1040,7 +1040,7 @@
val t = state |> Proof.raw_goal |> #goal |> prop_of
in
case Logic.count_prems t of
- 0 => (priority "No subgoal!"; ("none", state))
+ 0 => (Output.urgent_message "No subgoal!"; ("none", state))
| n =>
let
val t = Logic.goal_params t i |> fst