--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 04 19:00:49 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 04 19:00:49 2013 +0100
@@ -37,7 +37,7 @@
val minN = "min"
val messagesN = "messages"
val supported_proversN = "supported_provers"
-val killN = "kill"
+val kill_allN = "kill_all"
val running_proversN = "running_provers"
val running_learnersN = "running_learners"
val refresh_tptpN = "refresh_tptp"
@@ -395,7 +395,7 @@
messages opt_i
else if subcommand = supported_proversN then
supported_provers ctxt
- else if subcommand = killN then
+ else if subcommand = kill_allN then
(kill_provers (); kill_learners ())
else if subcommand = running_proversN then
running_provers ()