diff -r f190a6dbb29b -r 271a4a6af734 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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:05 2012 +0200
@@ -388,7 +388,7 @@
     else if subcommand = running_learnersN then
       running_learners ()
     else if subcommand = unlearnN then
-      mash_reset ctxt
+      mash_unlearn ctxt
     else if subcommand = refresh_tptpN then
       refresh_systems_on_tptp ()
     else