--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Sat Apr 19 19:03:32 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Sat Apr 19 19:52:02 2014 +0200
@@ -498,13 +498,4 @@
in () end
| NONE => error "Unknown proof context"))
-val _ = Session.protocol_handler "isabelle.Sledgehammer_Params$Handler"
-
-val _ = Isabelle_Process.protocol_command "Sledgehammer.provers"
- (fn [] =>
- let
- val this_thy = @{theory}
- val provers = space_implode " " (#provers (default_params this_thy []))
- in Output.protocol_message Markup.sledgehammer_provers [provers] end)
-
end;