src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML

     (if is_proof_method_multi_goal meth andalso n <> 1 then "[1]" else "")
   end
 
 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
 
 fun one_line_proof_text ctxt num_chained
     ((used_facts, (meth, play)), banner, subgoal, subgoal_count) =