--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 18 08:44:04 2012 +0200
@@ -36,8 +36,7 @@
val running_proversN = "running_provers"
val kill_proversN = "kill_provers"
val refresh_tptpN = "refresh_tptp"
-val mash_resetN = "mash_reset"
-val mash_learnN = "mash_learn"
+val reset_mashN = "reset_mash"
val auto = Unsynchronized.ref false
@@ -377,10 +376,8 @@
kill_provers ()
else if subcommand = refresh_tptpN then
refresh_systems_on_tptp ()
- else if subcommand = mash_resetN then
- mash_reset ()
- else if subcommand = mash_learnN then
- () (* TODO: implement *)
+ else if subcommand = reset_mashN then
+ mash_reset ctxt
else
error ("Unknown subcommand: " ^ quote subcommand ^ ".")
end