--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Oct 02 21:06:32 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Oct 02 21:15:25 2015 +0200
@@ -33,8 +33,6 @@
val runN = "run"
val supported_proversN = "supported_provers"
-val kill_learnersN = "kill_learners"
-val running_learnersN = "running_learners"
val refresh_tptpN = "refresh_tptp"
(** Sledgehammer commands **)
@@ -326,8 +324,6 @@
end
else if subcommand = supported_proversN then
supported_provers ctxt
- else if subcommand = kill_learnersN then
- kill_learners ()
else if subcommand = unlearnN then
mash_unlearn ()
else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse
@@ -343,8 +339,6 @@
[("preplay_timeout", ["0"])]))
fact_override (#facts (Proof.goal state))
(subcommand = learn_proverN orelse subcommand = relearn_proverN))
- else if subcommand = running_learnersN then
- running_learners ()
else if subcommand = refresh_tptpN then
refresh_systems_on_tptp ()
else