changeset 40132 | 7ee65dbffa31 |
parent 40113 | 1f61f0826e8a |
child 40222 | cd6d2b0a4096 |
--- a/src/HOL/Tools/try.ML Mon Oct 25 20:24:13 2010 +0200 +++ b/src/HOL/Tools/try.ML Mon Oct 25 21:06:56 2010 +0200 @@ -96,7 +96,7 @@ Pretty.markup Markup.hilite [Pretty.str message]]) else - tap (fn _ => priority message))) + tap (fn _ => Output.urgent_message message))) end val invoke_try = fst oo do_try false