--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Nov 23 16:15:17 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Nov 23 20:55:58 2016 +0100
@@ -324,10 +324,10 @@
else if subcommand = supported_proversN then
supported_provers ctxt
else if subcommand = unlearnN then
- mash_unlearn ()
+ mash_unlearn ctxt
else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse
subcommand = relearn_isarN orelse subcommand = relearn_proverN then
- (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ()
+ (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ctxt
else ();
mash_learn ctxt
(* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *)