1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Jan 18 14:33:16 2013 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Jan 18 16:06:45 2013 +0100
     1.3 @@ -1383,7 +1383,7 @@
     1.4  (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
     1.5     dangerous because their "exhaust" properties can easily lead to unsound ATP
     1.6     proofs. On the other hand, all HOL infinite types can be given the same
     1.7 -   models in first-order logic (via Löwenheim-Skolem). *)
     1.8 +   models in first-order logic (via Loewenheim-Skolem). *)
     1.9  
    1.10  fun should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
    1.11                               maybe_nonmono_Ts}

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 18 14:33:16 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 18 16:06:45 2013 +0100
     2.3 @@ -39,7 +39,7 @@
     2.4        -> (string * string list * (string * real) list * string list) list -> unit
     2.5      val relearn :
     2.6        Proof.context -> bool -> (string * string list) list -> unit
     2.7 -    val suggest :
     2.8 +    val query :
     2.9        Proof.context -> bool -> bool -> int
    2.10        -> string list * (string * real) list * string list -> string list
    2.11    end
    2.12 @@ -256,8 +256,8 @@
    2.13           elide_string 1000 (space_implode " " (map #1 relearns)));
    2.14       run_mash_tool ctxt overlord true 0 (relearns, str_of_relearn) (K ()))
    2.15  
    2.16 -fun suggest ctxt overlord learn_hints max_suggs (query as (_, feats, hints)) =
    2.17 -  (trace_msg ctxt (fn () => "MaSh suggest " ^ encode_features feats);
    2.18 +fun query ctxt overlord learn_hints max_suggs (query as (_, feats, hints)) =
    2.19 +  (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats);
    2.20     run_mash_tool ctxt overlord (learn_hints andalso not (null hints))
    2.21         max_suggs ([query], str_of_query learn_hints)
    2.22         (fn suggs =>
    2.23 @@ -808,8 +808,8 @@
    2.24                  chained |> filter (is_fact_in_graph access_G snd)
    2.25                          |> map (nickname_of_thm o snd)
    2.26              in
    2.27 -              (access_G, MaSh.suggest ctxt overlord learn max_facts
    2.28 -                                      (parents, feats, hints))
    2.29 +              (access_G, MaSh.query ctxt overlord learn max_facts
    2.30 +                                    (parents, feats, hints))
    2.31              end)
    2.32      val unknown = facts |> filter_out (is_fact_in_graph access_G snd)
    2.33    in find_mash_suggestions max_facts suggs facts chained unknown end