1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -33,10 +33,12 @@
     1.4  val minN = "min"
     1.5  val messagesN = "messages"
     1.6  val supported_proversN = "supported_provers"
     1.7 +val kill_proversN = "kill_provers"
     1.8  val running_proversN = "running_provers"
     1.9 -val kill_proversN = "kill_provers"
    1.10 +val kill_learnersN = "kill_learners"
    1.11 +val running_learnersN = "running_learners"
    1.12 +val unlearnN = "unlearn"
    1.13  val refresh_tptpN = "refresh_tptp"
    1.14 -val reset_mashN = "reset_mash"
    1.15  
    1.16  val auto = Unsynchronized.ref false
    1.17  
    1.18 @@ -374,14 +376,18 @@
    1.19        messages opt_i
    1.20      else if subcommand = supported_proversN then
    1.21        supported_provers ctxt
    1.22 +    else if subcommand = kill_proversN then
    1.23 +      kill_provers ()
    1.24      else if subcommand = running_proversN then
    1.25        running_provers ()
    1.26 -    else if subcommand = kill_proversN then
    1.27 -      kill_provers ()
    1.28 +    else if subcommand = kill_learnersN then
    1.29 +      kill_learners ()
    1.30 +    else if subcommand = running_learnersN then
    1.31 +      running_learners ()
    1.32 +    else if subcommand = unlearnN then
    1.33 +      mash_reset ctxt
    1.34      else if subcommand = refresh_tptpN then
    1.35        refresh_systems_on_tptp ()
    1.36 -    else if subcommand = reset_mashN then
    1.37 -      mash_reset ctxt
    1.38      else
    1.39        error ("Unknown subcommand: " ^ quote subcommand ^ ".")
    1.40    end