# HG changeset patch
# User wenzelm
# Date 1268494635 -3600
# Node ID c4a698ee83b407ff8af46f18189f8b88fcfc1a27
# Parent  22e6c38ebe2500d835ec94f16b93cf236a626bb4
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;

diff -r 22e6c38ebe25 -r c4a698ee83b4 src/HOL/Tools/arith_data.ML
--- 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;