1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jan 31 11:31:30 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jan 31 12:09:07 2013 +0100
     1.3 @@ -146,13 +146,18 @@
     1.4      val sugg_path = Path.explode sugg_file
     1.5      val cmd_file = temp_dir ^ "/mash_commands" ^ serial
     1.6      val cmd_path = Path.explode cmd_file
     1.7 +    val model_dir = File.shell_path (mash_model_dir ())
     1.8      val core =
     1.9        "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
    1.10        " --numberOfPredictions " ^ string_of_int max_suggs ^
    1.11        (* " --learnTheories" ^ *) (if save then " --saveModel" else "")
    1.12      val command =
    1.13 -      "\"$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py\" --quiet --outputDir " ^
    1.14 -      File.shell_path (mash_model_dir ()) ^ " --log " ^ log_file ^ " " ^ core ^
    1.15 +      "\"$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py\" --quiet" ^
    1.16 +      " --outputDir " ^ model_dir ^
    1.17 +      " --modelFile=" ^ model_dir ^ "/model.pickle" ^
    1.18 +      " --dictsFile=" ^ model_dir ^ "/dict.pickle" ^
    1.19 +      " --theoryFile=" ^ model_dir ^ "/theory.pickle" ^
    1.20 +      " --log " ^ log_file ^ " " ^ core ^
    1.21        " >& " ^ err_file
    1.22      fun run_on () =
    1.23        (Isabelle_System.bash command