# HG changeset patch
# User blanchet
# Date 1358521605 -3600
# Node ID 4179fa5c79fed7277409c6252b199dcef1ad731f
# Parent  3686bc0d4df2b9a1057a322a42c3a4ee36297622
tuning

diff -r 3686bc0d4df2 -r 4179fa5c79fe src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Jan 18 14:33:16 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Jan 18 16:06:45 2013 +0100
@@ -1383,7 +1383,7 @@
 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
    dangerous because their "exhaust" properties can easily lead to unsound ATP
    proofs. On the other hand, all HOL infinite types can be given the same
-   models in first-order logic (via Löwenheim-Skolem). *)
+   models in first-order logic (via Loewenheim-Skolem). *)
 
 fun should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
                              maybe_nonmono_Ts}
diff -r 3686bc0d4df2 -r 4179fa5c79fe src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 18 14:33:16 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 18 16:06:45 2013 +0100
@@ -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 suggest :
+    val query :
       Proof.context -> bool -> bool -> int
       -> string list * (string * real) list * string list -> string list
   end
@@ -256,8 +256,8 @@
          elide_string 1000 (space_implode " " (map #1 relearns)));
      run_mash_tool ctxt overlord true 0 (relearns, str_of_relearn) (K ()))
 
-fun suggest ctxt overlord learn_hints max_suggs (query as (_, feats, hints)) =
-  (trace_msg ctxt (fn () => "MaSh suggest " ^ encode_features feats);
+fun query ctxt overlord learn_hints max_suggs (query as (_, feats, hints)) =
+  (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats);
    run_mash_tool ctxt overlord (learn_hints andalso not (null hints))
        max_suggs ([query], str_of_query learn_hints)
        (fn suggs =>
@@ -808,8 +808,8 @@
                 chained |> filter (is_fact_in_graph access_G snd)
                         |> map (nickname_of_thm o snd)
             in
-              (access_G, MaSh.suggest ctxt overlord learn max_facts
-                                      (parents, feats, hints))
+              (access_G, MaSh.query ctxt overlord learn max_facts
+                                    (parents, feats, hints))
             end)
     val unknown = facts |> filter_out (is_fact_in_graph access_G snd)
   in find_mash_suggestions max_facts suggs facts chained unknown end