author | huffman |
Sun, 07 Mar 2010 09:57:30 -0800 | |
changeset 35636 | fe9b43a08187 |
parent 35635 | 90fffd5ff996 |
child 35637 | e0b2a6e773db |
--- 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;