make Sledgehammer a little bit less verbose in "try"

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 10:30:08 2011 +0200
@@ -174,7 +174,9 @@
       let
         val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
       in
-        (if outcome_code = someN then message else quote name ^ ": " ^ message)
+        (if outcome_code = someN then message
+         else if mode = Normal then quote name ^ ": " ^ message
+         else "")
         |> Async_Manager.break_into_chunks
         |> List.app Output.urgent_message;
         (outcome_code, state)