src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

   encode_str name ^
   (if Real.== (weight, 1.0) then "" else "=" ^ Markup.print_real weight)
 
 val encode_features = map encode_feature #> space_implode " "
 
+val str_of_saveless_shutdown = "S\n"
+
 fun str_of_learn (name, parents, feats, deps) =
   "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
   encode_features feats ^ "; " ^ encode_strs deps ^ "\n"
 
 fun str_of_relearn (name, deps) =

 struct
 
 fun unlearn ctxt =
   let val path = mash_model_dir () in
     trace_msg ctxt (K "MaSh unlearn");
+    run_mash_tool ctxt false ([()], K str_of_saveless_shutdown);
     try (File.fold_dir (fn file => fn _ =>
                            try File.rm (Path.append path (Path.basic file)))
                        path) NONE;
     ()
   end