src/HOL/Tools/Nitpick/nitpick.ML

       if auto then
         Unsynchronized.change state_ref o Proof.goal_message o K
         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
     fun pprint_d f = () |> debug ? pprint o f
     val print = pprint o curry Pretty.blk 0 o pstrs

   handle Exn.Interrupt =>
          if auto orelse #debug params then
            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."
 
 fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
                       step subst assm_ts orig_t =

   let
     val ctxt = Proof.context_of state
     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
         val assms = map term_of (Assumption.all_assms_of ctxt)
         val (subst, assms, t) = extract_fixed_frees ctxt (assms, t)