# HG changeset patch
# User blanchet
# Date 1357322449 -3600
# Node ID 58b0b44da54a02df0bd3666fc063310e7cd8947d
# Parent  60203cb4dbb87e20b9521a549be213ca63530ae2
renamed "kill" subcommand to avoid clash with "kill" keyword (which confuses Proof General and results in strange syntax highlighting)

diff -r 60203cb4dbb8 -r 58b0b44da54a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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 ()