reverted fe9b43a08187 -- "warning" is a perfectly normal way of tactics to emit spurious messages (although "arith" could be less chatty), while "priority" is a special Proof General protocol message;

--- a/src/HOL/Tools/arith_data.ML	Sat Mar 13 15:11:59 2010 +0100
+++ b/src/HOL/Tools/arith_data.ML	Sat Mar 13 16:37:15 2010 +0100
@@ -53,9 +53,9 @@
 
 fun gen_arith_tac verbose ctxt =
   let
-    val tactics = (Arith_Tactics.get o ProofContext.theory_of) ctxt
-    fun invoke (_, (name, tac)) k st = (if verbose
-      then priority ("Trying " ^ name ^ "...") else ();
+    val tactics = Arith_Tactics.get (ProofContext.theory_of ctxt);
+    fun invoke (_, (name, tac)) k st =
+     (if verbose then warning ("Trying " ^ name ^ "...") else ();
       tac verbose ctxt k st);
   in FIRST' (map invoke (rev tactics)) end;