src/HOL/Tools/try0.ML
changeset 63518 ae8fd6fe63a1
parent 62984 61b32a6d87e9
child 63690 48a2c88091d7
--- a/src/HOL/Tools/try0.ML	Sat Jul 16 18:56:43 2016 +0200
+++ b/src/HOL/Tools/try0.ML	Sat Jul 16 19:35:27 2016 +0200
@@ -143,7 +143,7 @@
              Auto_Try => "Auto Try0 found a proof"
            | Try => "Try0 found a proof"
            | Normal => "Try this") ^ ": " ^
-          Active.sendback_markup [Markup.padding_command]
+          Active.sendback_markup_command
               ((if Thm.nprems_of (#goal (Proof.goal st)) = 1 then "by"
                 else "apply") ^ " " ^ command) ^
           (case xs of