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