# HG changeset patch
# User blanchet
# Date 1306485008 -7200
# Node ID b10775a669d15708d549ae14e4b7e0e1a28a0919
# Parent  0f15575a6465f27b6e9f53b9ec734219e05b176e
make Sledgehammer a little bit less verbose in "try"

diff -r 0f15575a6465 -r b10775a669d1 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- 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)