src/HOL/Tools/try.ML
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