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