# HG changeset patch
# User blanchet
# Date 1359630547 -3600
# Node ID 461fdbbdb912e54ec148a8f4cc14750168adb463
# Parent  c9adb50f74ad6da6f2405f121040cca47c4ddf1a
adapted to new MaSh interface

diff -r c9adb50f74ad -r 461fdbbdb912 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jan 31 11:31:30 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jan 31 12:09:07 2013 +0100
@@ -146,13 +146,18 @@
     val sugg_path = Path.explode sugg_file
     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 ^
       (* " --learnTheories" ^ *) (if save then " --saveModel" else "")
     val command =
-      "\"$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py\" --quiet --outputDir " ^
-      File.shell_path (mash_model_dir ()) ^ " --log " ^ log_file ^ " " ^ core ^
+      "\"$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py\" --quiet" ^
+      " --outputDir " ^ model_dir ^
+      " --modelFile=" ^ model_dir ^ "/model.pickle" ^
+      " --dictsFile=" ^ model_dir ^ "/dict.pickle" ^
+      " --theoryFile=" ^ model_dir ^ "/theory.pickle" ^
+      " --log " ^ log_file ^ " " ^ core ^
       " >& " ^ err_file
     fun run_on () =
       (Isabelle_System.bash command