src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
changeset 63518 ae8fd6fe63a1
parent 62219 dbac573b27e7
child 63692 1bc4bc2c9fd1
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sat Jul 16 18:56:43 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sat Jul 16 19:35:27 2016 +0200
@@ -180,7 +180,7 @@
 
 fun try_command_line banner play command =
   let val s = string_of_play_outcome play in
-    banner ^ ": " ^ Active.sendback_markup [Markup.padding_command] command ^
+    banner ^ ": " ^ Active.sendback_markup_command command ^
     (s |> s <> "" ? enclose " (" ")") ^ "."
   end