--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Jan 31 16:09:23 2022 +0100
@@ -183,8 +183,7 @@
fun try_command_line banner play command =
let val s = string_of_play_outcome play in
- banner ^ Active.sendback_markup_command command ^
- (s |> s <> "" ? enclose " (" ")")
+ banner ^ Active.sendback_markup_command command ^ (s |> s <> "" ? enclose " (" ")")
end
fun one_line_proof_text _ num_chained