diff -r 81a1295c69ad -r 20aa19ecf2cc src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Mon Nov 03 09:25:23 2014 +0100
+++ b/src/HOL/Tools/try0.ML	Mon Nov 03 14:31:15 2014 +0100
@@ -129,7 +129,7 @@
       ();
     (case par_map (fn f => f mode timeout_opt quad st) apply_methods of
       [] =>
-      (if mode = Normal then writeln "No proof found." else (); (false, (noneN, st)))
+      (if mode = Normal then writeln "No proof found." else (); (false, (noneN, [])))
     | xs as (name, command, _) :: _ =>
       let
         val xs = xs |> map (fn (name, _, n) => (n, name))
@@ -147,12 +147,10 @@
             [(_, ms)] => " (" ^ time_string ms ^ ")."
           | xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ").")
       in
-        (true, (name,
-           st
-           |> (if mode = Auto_Try then
-                 Proof.goal_message (fn () => Pretty.markup Markup.information [Pretty.str message])
-               else
-                 tap (fn _ => writeln message))))
+        (true,
+          (name,
+            if mode = Auto_Try then [Markup.markup Markup.information message]
+            else (writeln message; [])))
       end)
   end;