diff -r 1133b9e83f09 -r 54f3c94c5ec1 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Aug 20 14:36:22 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Aug 20 14:36:22 2013 +0200
@@ -145,7 +145,7 @@
    xs |> chunk_list 500 |> List.app (File.append path o implode o map f))
   handle IO.Io _ => ()
 
-fun run_mash_tool ctxt overlord save write_cmds read_suggs =
+fun run_mash_tool ctxt overlord write_cmds read_suggs =
   let
     val (temp_dir, serial) =
       if overlord then (getenv "ISABELLE_HOME_USER", "")
@@ -157,10 +157,7 @@
     val cmd_file = temp_dir ^ "/mash_commands" ^ serial
     val cmd_path = Path.explode cmd_file
     val model_dir = File.shell_path (mash_model_dir ())
-    val core =
-      "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
-      " --numberOfPredictions " ^ string_of_int max_suggs ^
-      (if save then " --saveModel" else "")
+    val core = "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file
     val command =
       "cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; " ^
       "./mash.py --quiet" ^
@@ -262,17 +259,17 @@
   | learn ctxt overlord learns =
     (trace_msg ctxt (fn () => "MaSh learn " ^
          elide_string 1000 (space_implode " " (map #1 learns)));
-     run_mash_tool ctxt overlord true (learns, str_of_learn) (K ()))
+     run_mash_tool ctxt overlord (learns, str_of_learn) (K ()))
 
 fun relearn _ _ [] = ()
   | relearn ctxt overlord relearns =
     (trace_msg ctxt (fn () => "MaSh relearn " ^
          elide_string 1000 (space_implode " " (map #1 relearns)));
-     run_mash_tool ctxt overlord true (relearns, str_of_relearn) (K ()))
+     run_mash_tool ctxt overlord (relearns, str_of_relearn) (K ()))
 
 fun query ctxt overlord max_suggs (query as (learns, hints, _, feats)) =
   (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats);
-   run_mash_tool ctxt overlord false ([query], str_of_query max_suggs)
+   run_mash_tool ctxt overlord ([query], str_of_query max_suggs)
        (fn suggs =>
            case suggs () of
              [] => []