src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sat Dec 18 14:30:13 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sat Dec 18 23:11:49 2021 +0100
@@ -394,6 +394,7 @@
         val i = 1
       in
         run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (silence_state state)
+        |> apsnd (map_prod short_string_of_sledgehammer_outcome single)
       end}
 
 val _ =