# HG changeset patch
# User blanchet
# Date 1356733911 -3600
# Node ID 87961472b4040f11f9f070ffdfd3f9a1ede69f86
# Parent  12c097ff32414cc8ae65b1c314bfb6b0b2785b0a
tuned ML function name

diff -r 12c097ff3241 -r 87961472b404 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Fri Dec 28 21:03:39 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Fri Dec 28 23:31:51 2012 +0100
@@ -72,7 +72,7 @@
     fun solve_goal (j, line) =
       if in_range range j then
         let
-          val (name, suggs) = extract_query line
+          val (name, suggs) = extract_suggestions line
           val th =
             case find_first (fn (_, th) => nickname_of_thm th = name) facts of
               SOME (_, th) => th
diff -r 12c097ff3241 -r 87961472b404 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Dec 28 21:03:39 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Dec 28 23:31:51 2012 +0100
@@ -29,7 +29,7 @@
   val unescape_meta : string -> string
   val unescape_metas : string -> string list
   val encode_features : (string * real) list -> string
-  val extract_query : string -> string * (string * real) list
+  val extract_suggestions : string -> string * (string * real) list
 
   structure MaSh:
   sig
@@ -39,7 +39,7 @@
       -> (string * string list * (string * real) list * string list) list -> unit
     val relearn :
       Proof.context -> bool -> (string * string list) list -> unit
-    val query :
+    val suggest :
       Proof.context -> bool -> int -> string list * (string * real) list
       -> (string * real) list
   end
@@ -213,7 +213,7 @@
   | [name] => SOME (unescape_meta name, 1.0)
   | _ => NONE
 
-fun extract_query line =
+fun extract_suggestions line =
   case space_explode ":" line of
     [goal, suggs] =>
     (unescape_meta goal,
@@ -244,14 +244,14 @@
          elide_string 1000 (space_implode " " (map #1 relearns)));
      run_mash_tool ctxt overlord true 0 (relearns, str_of_relearn) (K ()))
 
-fun query ctxt overlord max_suggs (query as (_, feats)) =
-  (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats);
+fun suggest ctxt overlord max_suggs (query as (_, feats)) =
+  (trace_msg ctxt (fn () => "MaSh suggest " ^ encode_features feats);
    run_mash_tool ctxt overlord false max_suggs
        ([query], str_of_query)
        (fn suggs =>
            case suggs () of
              [] => []
-           | suggs => snd (extract_query (List.last suggs)))
+           | suggs => snd (extract_suggestions (List.last suggs)))
    handle List.Empty => [])
 
 end;
@@ -788,7 +788,7 @@
               val feats =
                 features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
             in
-              (access_G, MaSh.query ctxt overlord max_facts (parents, feats))
+              (access_G, MaSh.suggest ctxt overlord max_facts (parents, feats))
             end)
     val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
     val unknown = facts |> filter_out (is_fact_in_graph access_G)