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;