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 @@ -36,8 +36,7 @@
     1.4  val running_proversN = "running_provers"
     1.5  val kill_proversN = "kill_provers"
     1.6  val refresh_tptpN = "refresh_tptp"
     1.7 -val mash_resetN = "mash_reset"
     1.8 -val mash_learnN = "mash_learn"
     1.9 +val reset_mashN = "reset_mash"
    1.10  
    1.11  val auto = Unsynchronized.ref false
    1.12  
    1.13 @@ -377,10 +376,8 @@
    1.14        kill_provers ()
    1.15      else if subcommand = refresh_tptpN then
    1.16        refresh_systems_on_tptp ()
    1.17 -    else if subcommand = mash_resetN then
    1.18 -      mash_reset ()
    1.19 -    else if subcommand = mash_learnN then
    1.20 -      () (* TODO: implement *)
    1.21 +    else if subcommand = reset_mashN then
    1.22 +      mash_reset ctxt
    1.23      else
    1.24        error ("Unknown subcommand: " ^ quote subcommand ^ ".")
    1.25    end