adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)

--- a/src/Doc/Sledgehammer/document/root.tex	Wed Dec 12 00:14:58 2012 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Dec 12 00:24:06 2012 +0100
@@ -694,9 +694,9 @@
 proofs. This happens automatically at Sledgehammer invocations if the
 \textit{learn} option (\S\ref{relevance-filter}) is enabled.
 
-\item[\labelitemi] \textbf{\textit{learn\_atp}:} Invokes MaSh on the current
-theory to process all the available facts, learning from ATP-generated proofs.
-The ATP to use and its timeout can be set using the
+\item[\labelitemi] \textbf{\textit{learn\_prover}:} Invokes MaSh on the current
+theory to process all the available facts, learning from proofs generated by
+automatic provers. The prover to use and its timeout can be set using the
 \textit{prover} (\S\ref{mode-of-operation}) and \textit{timeout}
 (\S\ref{timeouts}) options. It is recommended to perform learning using an
 efficient first-order ATP (such as E, SPASS, and Vampire) as opposed to a
@@ -705,8 +705,8 @@
 \item[\labelitemi] \textbf{\textit{relearn\_isar}:} Same as \textit{unlearn}
 followed by \textit{learn\_isar}.
 
-\item[\labelitemi] \textbf{\textit{relearn\_atp}:} Same as \textit{unlearn}
-followed by \textit{learn\_atp}.
+\item[\labelitemi] \textbf{\textit{relearn\_prover}:} Same as \textit{unlearn}
+followed by \textit{learn\_prover}.
 
 \item[\labelitemi] \textbf{\textit{running\_learners}:} Prints information about
 currently running machine learners, including elapsed runtime and remaining
@@ -719,8 +719,8 @@
 Sledgehammer's behavior can be influenced by various \qty{options}, which can be
 specified in brackets after the \textbf{sledgehammer} command. The
 \qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1,
-\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional. For
-example:
+\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional.
+For example:
 
 \prew
 \textbf{sledgehammer} [\textit{isar\_proofs}, \,\textit{timeout} = 120]

--- a/src/HOL/TPTP/MaSh_Eval.thy	Wed Dec 12 00:14:58 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Wed Dec 12 00:24:06 2012 +0100
@@ -17,7 +17,7 @@
 declare [[sledgehammer_instantiate_inducts]]
 
 ML {*
-! Multithreading.max_threads
+!Multithreading.max_threads
 *}
 
 ML {*

--- a/src/HOL/TPTP/MaSh_Export.thy	Wed Dec 12 00:14:58 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Dec 12 00:24:06 2012 +0100
@@ -52,7 +52,8 @@
 
 ML {*
 if do_it then
-  generate_isar_dependencies @{context} thys false (prefix ^ "mash_dependencies")
+  generate_isar_dependencies @{context} thys false
+      (prefix ^ "mash_dependencies")
 else
   ()
 *}
@@ -66,21 +67,24 @@
 
 ML {*
 if do_it then
-  generate_mepo_suggestions @{context} params thys 1024 (prefix ^ "mash_mepo_suggestions")
+  generate_mepo_suggestions @{context} params thys 1024
+      (prefix ^ "mash_mepo_suggestions")
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_atp_dependencies @{context} params thys false (prefix ^ "mash_atp_dependencies")
+  generate_prover_dependencies @{context} params thys false
+      (prefix ^ "mash_prover_dependencies")
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_atp_commands @{context} params thys (prefix ^ "mash_atp_commands")
+  generate_prover_commands @{context} params thys
+      (prefix ^ "mash_prover_commands")
 else
   ()
 *}

--- a/src/HOL/TPTP/mash_export.ML	Wed Dec 12 00:14:58 2012 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Wed Dec 12 00:24:06 2012 +0100
@@ -15,11 +15,11 @@
     Proof.context -> string -> theory list -> bool -> string -> unit
   val generate_isar_dependencies :
     Proof.context -> theory list -> bool -> string -> unit
-  val generate_atp_dependencies :
+  val generate_prover_dependencies :
     Proof.context -> params -> theory list -> bool -> string -> unit
   val generate_isar_commands :
     Proof.context -> string -> theory list -> string -> unit
-  val generate_atp_commands :
+  val generate_prover_commands :
     Proof.context -> params -> theory list -> string -> unit
   val generate_mepo_suggestions :
     Proof.context -> params -> theory list -> int -> string -> unit
@@ -97,15 +97,15 @@
       in File.append path s end
   in List.app do_fact facts end
 
-fun isar_or_atp_dependencies_of ctxt params_opt facts all_names th =
+fun isar_or_prover_dependencies_of ctxt params_opt facts all_names th =
   (case params_opt of
      SOME (params as {provers = prover :: _, ...}) =>
-     atp_dependencies_of ctxt params prover 0 facts all_names th |> snd
+     prover_dependencies_of ctxt params prover 0 facts all_names th |> snd
    | NONE => isar_dependencies_of all_names th)
   |> these
 
-fun generate_isar_or_atp_dependencies ctxt params_opt thys include_thys
-                                      file_name =
+fun generate_isar_or_prover_dependencies ctxt params_opt thys include_thys
+                                         file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
@@ -118,18 +118,18 @@
       let
         val name = nickname_of th
         val deps =
-          isar_or_atp_dependencies_of ctxt params_opt facts all_names th
+          isar_or_prover_dependencies_of ctxt params_opt facts all_names th
         val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
       in File.append path s end
   in List.app do_thm ths end
 
 fun generate_isar_dependencies ctxt =
-  generate_isar_or_atp_dependencies ctxt NONE
+  generate_isar_or_prover_dependencies ctxt NONE
 
-fun generate_atp_dependencies ctxt params =
-  generate_isar_or_atp_dependencies ctxt (SOME params)
+fun generate_prover_dependencies ctxt params =
+  generate_isar_or_prover_dependencies ctxt (SOME params)
 
-fun generate_isar_or_atp_commands ctxt prover params_opt thys file_name =
+fun generate_isar_or_prover_commands ctxt prover params_opt thys file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
@@ -144,7 +144,7 @@
         val feats =
           features_of ctxt prover (theory_of_thm th) stature [prop_of th]
         val deps =
-          isar_or_atp_dependencies_of ctxt params_opt facts all_names th
+          isar_or_prover_dependencies_of ctxt params_opt facts all_names th
         val kind = Thm.legacy_get_kind th
         val core =
           escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
@@ -159,10 +159,10 @@
   in fold do_fact new_facts parents; () end
 
 fun generate_isar_commands ctxt prover =
-  generate_isar_or_atp_commands ctxt prover NONE
+  generate_isar_or_prover_commands ctxt prover NONE
 
-fun generate_atp_commands ctxt (params as {provers = prover :: _, ...}) =
-  generate_isar_or_atp_commands ctxt prover (SOME params)
+fun generate_prover_commands ctxt (params as {provers = prover :: _, ...}) =
+  generate_isar_or_prover_commands ctxt prover (SOME params)
 
 fun generate_mepo_suggestions ctxt (params as {provers, ...}) thys max_relevant
                               file_name =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Dec 12 00:14:58 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Dec 12 00:24:06 2012 +0100
@@ -367,7 +367,7 @@
     (if i = 1 then "" else " " ^ string_of_int i)
   end
 
-val default_learn_atp_timeout = 0.5
+val default_learn_prover_timeout = 0.5
 
 fun hammer_away override_params subcommand opt_i fact_override state =
   let
@@ -404,21 +404,22 @@
       running_provers ()
     else if subcommand = unlearnN then
       mash_unlearn ctxt
-    else if subcommand = learn_isarN orelse subcommand = learn_atpN orelse
-            subcommand = relearn_isarN orelse subcommand = relearn_atpN then
-      (if subcommand = relearn_isarN orelse subcommand = relearn_atpN then
+    else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse
+            subcommand = relearn_isarN orelse subcommand = relearn_proverN then
+      (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then
          mash_unlearn ctxt
        else
          ();
-       mash_learn ctxt (get_params Normal ctxt
-                           ([("timeout",
-                              [string_of_real default_learn_atp_timeout]),
-                             ("slice", ["false"])] @
-                            override_params @
-                            [("minimize", ["true"]),
-                             ("preplay_timeout", ["0"])]))
-                  fact_override (#facts (Proof.goal state))
-                  (subcommand = learn_atpN orelse subcommand = relearn_atpN))
+       mash_learn ctxt
+           (get_params Normal ctxt
+                ([("timeout",
+                   [string_of_real default_learn_prover_timeout]),
+                  ("slice", ["false"])] @
+                 override_params @
+                 [("minimize", ["true"]),
+                  ("preplay_timeout", ["0"])]))
+           fact_override (#facts (Proof.goal state))
+           (subcommand = learn_proverN orelse subcommand = relearn_proverN))
     else if subcommand = running_learnersN then
       running_learners ()
     else if subcommand = refresh_tptpN then

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Dec 12 00:14:58 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Dec 12 00:24:06 2012 +0100
@@ -20,9 +20,9 @@
   val meshN : string
   val unlearnN : string
   val learn_isarN : string
-  val learn_atpN : string
+  val learn_proverN : string
   val relearn_isarN : string
-  val relearn_atpN : string
+  val relearn_proverN : string
   val fact_filters : string list
   val escape_meta : string -> string
   val escape_metas : string list -> string
@@ -55,7 +55,7 @@
     Proof.context -> string -> theory -> stature -> term list
     -> (string * real) list
   val isar_dependencies_of : unit Symtab.table -> thm -> string list option
-  val atp_dependencies_of :
+  val prover_dependencies_of :
     Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
     -> thm -> bool * string list option
   val weight_mash_facts : ('a * thm) list -> (('a * thm) * real) list
@@ -105,9 +105,9 @@
 
 val unlearnN = "unlearn"
 val learn_isarN = "learn_isar"
-val learn_atpN = "learn_atp"
+val learn_proverN = "learn_prover"
 val relearn_isarN = "relearn_isar"
-val relearn_atpN = "relearn_atp"
+val relearn_proverN = "relearn_prover"
 
 fun mash_model_dir () =
   Path.explode "$ISABELLE_HOME_USER/mash" |> tap Isabelle_System.mkdir
@@ -248,15 +248,16 @@
 
 (*** Middle-level communication with MaSh ***)
 
-datatype proof_kind = Isar_Proof | ATP_Proof | Isar_Proof_wegen_ATP_Flop
+datatype proof_kind =
+  Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop
 
 fun str_of_proof_kind Isar_Proof = "i"
-  | str_of_proof_kind ATP_Proof = "a"
-  | str_of_proof_kind Isar_Proof_wegen_ATP_Flop = "x"
+  | str_of_proof_kind Automatic_Proof = "a"
+  | str_of_proof_kind Isar_Proof_wegen_Prover_Flop = "x"
 
 fun proof_kind_of_str "i" = Isar_Proof
-  | proof_kind_of_str "a" = ATP_Proof
-  | proof_kind_of_str "x" = Isar_Proof_wegen_ATP_Flop
+  | proof_kind_of_str "a" = Automatic_Proof
+  | proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop
 
 (* FIXME: Here a "Graph.update_node" function would be useful *)
 fun update_fact_graph_node (name, kind) =
@@ -596,7 +597,8 @@
 (* Too many dependencies is a sign that a decision procedure is at work. There
    isn't much to learn from such proofs. *)
 val max_dependencies = 20
-val atp_dependency_default_max_facts = 50
+
+val prover_dependency_default_max_facts = 50
 
 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
 val typedef_deps = [@{thm CollectI} |> nickname_of]
@@ -634,8 +636,8 @@
 fun isar_dependencies_of all_names th =
   th |> thms_in_proof (SOME all_names) |> trim_dependencies th
 
-fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
-                        auto_level facts all_names th =
+fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
+                           auto_level facts all_names th =
   case isar_dependencies_of all_names th of
     SOME [] => (false, SOME [])
   | isar_deps =>
@@ -653,11 +655,12 @@
           SOME ((name, status), th) => accum @ [((name, status), th)]
         | NONE => accum (* shouldn't happen *)
       val facts =
-        facts |> mepo_suggested_facts ctxt params prover
-                     (max_facts |> the_default atp_dependency_default_max_facts)
-                     NONE hyp_ts concl_t
-              |> fold (add_isar_dep facts) (these isar_deps)
-              |> map fix_name
+        facts
+        |> mepo_suggested_facts ctxt params prover
+               (max_facts |> the_default prover_dependency_default_max_facts)
+               NONE hyp_ts concl_t
+        |> fold (add_isar_dep facts) (these isar_deps)
+        |> map fix_name
     in
       if verbose andalso auto_level = 0 then
         let val num_facts = length facts in
@@ -680,7 +683,7 @@
            ();
          case used_facts |> map fst |> trim_dependencies th of
            NONE => (false, isar_deps)
-         | atp_deps => (true, atp_deps))
+         | prover_deps => (true, prover_deps))
       | _ => (false, isar_deps)
     end
 
@@ -789,12 +792,12 @@
     fun maybe_rep_from from (accum as (parents, graph)) =
       try_graph ctxt "updating graph" accum (fn () =>
           (from :: parents, Graph.add_edge_acyclic (from, name) graph))
-    val graph = graph |> update_fact_graph_node (name, ATP_Proof)
+    val graph = graph |> update_fact_graph_node (name, Automatic_Proof)
     val (deps, _) = ([], graph) |> fold maybe_rep_from deps
   in ((name, deps) :: reps, graph) end
 
 fun flop_wrt_fact_graph name =
-  update_fact_graph_node (name, Isar_Proof_wegen_ATP_Flop)
+  update_fact_graph_node (name, Isar_Proof_wegen_Prover_Flop)
 
 val learn_timeout_slack = 2.0
 
@@ -835,7 +838,7 @@
 
 (* The timeout is understood in a very slack fashion. *)
 fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover
-                     auto_level atp learn_timeout facts =
+                     auto_level run_prover learn_timeout facts =
   let
     val timer = Timer.startRealTimer ()
     fun next_commit_time () =
@@ -845,11 +848,13 @@
       facts |> List.partition (is_fact_in_graph fact_G)
             ||> sort (thm_ord o pairself snd)
   in
-    if null new_facts andalso (not atp orelse null old_facts) then
+    if null new_facts andalso (not run_prover orelse null old_facts) then
       if auto_level < 2 then
-        "No new " ^ (if atp then "ATP" else "Isar") ^ " proofs to learn." ^
-        (if auto_level = 0 andalso not atp then
-           "\n\nHint: Try " ^ sendback learn_atpN ^ " to learn from ATP proofs."
+        "No new " ^ (if run_prover then "automatic" else "Isar") ^
+        " proofs to learn." ^
+        (if auto_level = 0 andalso not run_prover then
+           "\n\nHint: Try " ^ sendback learn_proverN ^
+           " to learn from automatic provers."
          else
            "")
       else
@@ -862,8 +867,9 @@
         fun deps_of status th =
           if status = Non_Rec_Def orelse status = Rec_Def then
             SOME []
-          else if atp then
-            atp_dependencies_of ctxt params prover auto_level facts all_names th
+          else if run_prover then
+            prover_dependencies_of ctxt params prover auto_level facts all_names
+                                   th
             |> (fn (false, _) => NONE | (true, deps) => deps)
           else
             isar_dependencies_of all_names th
@@ -894,7 +900,7 @@
            if not last andalso auto_level = 0 then
              let val num_proofs = length adds + length reps in
                "Learned " ^ string_of_int num_proofs ^ " " ^
-               (if atp then "ATP" else "Isar") ^ " proof" ^
+               (if run_prover then "automatic" else "Isar") ^ " proof" ^
                plural_s num_proofs ^ " in the last " ^
                string_from_time commit_timeout ^ "."
                |> Output.urgent_message
@@ -950,7 +956,7 @@
               val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
             in ((reps, flops), (n, next_commit, timed_out)) end
         val n =
-          if not atp orelse null old_facts then
+          if not run_prover orelse null old_facts then
             n
           else
             let
@@ -962,8 +968,8 @@
                 random_range 0 max_isar
                 + (case kind_of_proof th of
                      Isar_Proof => 0
-                   | ATP_Proof => 2 * max_isar
-                   | Isar_Proof_wegen_ATP_Flop => max_isar)
+                   | Automatic_Proof => 2 * max_isar
+                   | Isar_Proof_wegen_Prover_Flop => max_isar)
                 - 500 * (th |> isar_dependencies_of all_names
                             |> Option.map length
                             |> the_default max_dependencies)
@@ -978,7 +984,7 @@
       in
         if verbose orelse auto_level < 2 then
           "Learned " ^ string_of_int n ^ " nontrivial " ^
-          (if atp then "ATP" else "Isar") ^ " proof" ^ plural_s n ^
+          (if run_prover then "automatic" else "Isar") ^ " proof" ^ plural_s n ^
           (if verbose then
              " in " ^ string_from_time (Timer.checkRealTimer timer)
            else
@@ -989,7 +995,7 @@
   end
 
 fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained
-               atp =
+               run_prover =
   let
     val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     val ctxt = ctxt |> Config.put instantiate_inducts false
@@ -998,17 +1004,19 @@
                        @{prop True}
     val num_facts = length facts
     val prover = hd provers
-    fun learn auto_level atp =
-      mash_learn_facts ctxt params prover auto_level atp infinite_timeout facts
+    fun learn auto_level run_prover =
+      mash_learn_facts ctxt params prover auto_level run_prover infinite_timeout
+                       facts
       |> Output.urgent_message
   in
-    if atp then
+    if run_prover then
       ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
-       plural_s num_facts ^ " for ATP proofs (" ^ quote prover ^ " timeout: " ^
-       string_from_time timeout ^ ").\n\nCollecting Isar proofs first..."
+       plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^
+       " timeout: " ^ string_from_time timeout ^
+       ").\n\nCollecting Isar proofs first..."
        |> Output.urgent_message;
        learn 1 false;
-       "Now collecting ATP proofs. This may take several hours. You can \
+       "Now collecting automatic proofs. This may take several hours. You can \
        \safely stop the learning process at any point."
        |> Output.urgent_message;
        learn 0 true)