--- a/src/HOL/Tools/try0.ML Sat Jul 13 12:39:45 2013 +0200
+++ b/src/HOL/Tools/try0.ML Sat Jul 13 13:25:42 2013 +0200
@@ -140,13 +140,12 @@
Active.sendback_markup
((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
- "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
+ "\n(" ^ space_implode "; " (map time_string xs) ^ ")."
in
(true, (s, st |> (if mode = Auto_Try then
Proof.goal_message
- (fn () => Pretty.chunks [Pretty.str "",
- Pretty.markup Markup.intensify
- [Pretty.str message]])
+ (fn () => Pretty.markup Markup.information
+ [Pretty.str message])
else
tap (fn _ => Output.urgent_message message))))
end