# HG changeset patch
# User blanchet
# Date 1377002182 -7200
# Node ID db5e1b53bbfce0bc912d059cf3f50e3944a58c77
# Parent  bc129252bba0efd898b7011f6033d65f84a56566
tuning

diff -r bc129252bba0 -r db5e1b53bbfc src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Aug 20 11:36:27 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Aug 20 14:36:22 2013 +0200
@@ -160,14 +160,13 @@
     val core =
       "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
       " --numberOfPredictions " ^ string_of_int max_suggs ^
-      (* " --learnTheories" ^ *) (if save then " --saveModel" else "")
+      (if save then " --saveModel" else "")
     val command =
       "cd \"$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 () =
@@ -232,8 +231,7 @@
   "? " ^ encode_strs parents ^ "; " ^ encode_features feats ^
   (if null hints then "" else "; " ^ encode_strs hints) ^ "\n"
 
-(* The weights currently returned by "mash.py" are too spaced out to make any
-   sense. *)
+(* The suggested weights don't make much sense. *)
 fun extract_suggestion sugg =
   case space_explode "=" sugg of
     [name, _ (* weight *)] =>