# HG changeset patch
# User blanchet
# Date 1377002182 -7200
# Node ID 5c7780d21d248413a1df368eaf58b38d08a65f0d
# Parent  db5e1b53bbfce0bc912d059cf3f50e3944a58c77
adapted to new MaSh syntax

diff -r db5e1b53bbfc -r 5c7780d21d24 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 max_suggs write_cmds read_suggs =
+fun run_mash_tool ctxt overlord save write_cmds read_suggs =
   let
     val (temp_dir, serial) =
       if overlord then (getenv "ISABELLE_HOME_USER", "")
@@ -226,9 +226,10 @@
 fun str_of_relearn (name, deps) =
   "p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n"
 
-fun str_of_query (learns, hints, parents, feats) =
+fun str_of_query max_suggs (learns, hints, parents, feats) =
   implode (map str_of_learn learns) ^
-  "? " ^ encode_strs parents ^ "; " ^ encode_features feats ^
+  "? " ^ string_of_int max_suggs ^ " # " ^ encode_strs parents ^ "; " ^
+  encode_features feats ^
   (if null hints then "" else "; " ^ encode_strs hints) ^ "\n"
 
 (* The suggested weights don't make much sense. *)
@@ -261,17 +262,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 0 (learns, str_of_learn) (K ()))
+     run_mash_tool ctxt overlord true (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 0 (relearns, str_of_relearn) (K ()))
+     run_mash_tool ctxt overlord true (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 max_suggs ([query], str_of_query)
+   run_mash_tool ctxt overlord false ([query], str_of_query max_suggs)
        (fn suggs =>
            case suggs () of
              [] => []