--- a/src/HOL/Tools/try0.ML Sat Aug 17 14:13:18 2013 +0200
+++ b/src/HOL/Tools/try0.ML Sat Aug 17 19:13:28 2013 +0200
@@ -137,7 +137,7 @@
Auto_Try => "Auto Try0 found a proof"
| Try => "Try0 found a proof"
| Normal => "Try this") ^ ": " ^
- Active.sendback_markup (if mode = Auto_Try then [Markup.padding_command] else [])
+ Active.sendback_markup [Markup.padding_command]
((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
"\n(" ^ space_implode "; " (map time_string xs) ^ ")."