# HG changeset patch
# User huffman
# Date 1267984650 28800
# Node ID fe9b43a08187c444a67e9f56197317de72484074
# Parent  90fffd5ff996beb3c013f1875678728afef18687
arith tactic uses 'priority' instead of 'warning' to print messages

diff -r 90fffd5ff996 -r fe9b43a08187 src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Sun Mar 07 09:21:16 2010 -0800
+++ b/src/HOL/Tools/arith_data.ML	Sun Mar 07 09:57:30 2010 -0800
@@ -55,7 +55,7 @@
   let
     val tactics = (Arith_Tactics.get o ProofContext.theory_of) ctxt
     fun invoke (_, (name, tac)) k st = (if verbose
-      then warning ("Trying " ^ name ^ "...") else ();
+      then priority ("Trying " ^ name ^ "...") else ();
       tac verbose ctxt k st);
   in FIRST' (map invoke (rev tactics)) end;