src/HOL/Tools/try0.ML

--- a/src/HOL/Tools/try0.ML	Tue Dec 23 16:00:38 2014 +0100
+++ b/src/HOL/Tools/try0.ML	Tue Dec 23 20:46:42 2014 +0100
@@ -147,10 +147,7 @@
             [(_, ms)] => " (" ^ time_string ms ^ ")."
           | xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ").")
       in
-        (true,
-          (name,
-            if mode = Auto_Try then [Markup.markup Markup.information message]
-            else (writeln message; [])))
+        (true, (name, if mode = Auto_Try then [message] else (writeln message; [])))
       end)
   end;