src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
changeset 56333 38f1422ef473
parent 56081 72fad75baf7e
child 56467 8d7d6f17c6a7
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sun Mar 30 21:24:59 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Mar 31 10:28:08 2014 +0200
@@ -505,6 +505,6 @@
     let
       val this_thy = @{theory}
       val provers = space_implode " " (#provers (default_params this_thy []))
-    in Output.protocol_message Markup.sledgehammer_provers provers end)
+    in Output.protocol_message Markup.sledgehammer_provers [provers] end)
 
 end;