merge

--- a/src/Doc/Sledgehammer/document/root.tex	Mon Dec 10 16:27:03 2012 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Mon Dec 10 16:38:20 2012 +0100
@@ -417,10 +417,10 @@
 relies on an external Python tool that applies machine learning to
 the problem of finding relevant facts.
 
-\item[\labelitemi] The \emph{Mesh} filter combines MePo and MaSh.
+\item[\labelitemi] The \emph{MeSh} filter combines MePo and MaSh.
 \end{enum}
 
-The default is either MePo or Mesh, depending on whether the environment
+The default is either MePo or MeSh, depending on whether the environment
 variable \texttt{MASH} is set and what class of provers the target prover
 belongs to (\S\ref{relevance-filter}).
 
@@ -1062,7 +1062,7 @@
 
 \item[\labelitemi] \textbf{\textit{mesh}:} A combination of MePo and MaSh.
 
-\item[\labelitemi] \textbf{\textit{smart}:} Use Mesh if MaSh is
+\item[\labelitemi] \textbf{\textit{smart}:} Use MeSh if MaSh is
 enabled and the target prover is an ATP; otherwise, use MePo.
 \end{enum}
 

--- a/src/HOL/TPTP/MaSh_Eval.thy	Mon Dec 10 16:27:03 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Mon Dec 10 16:38:20 2012 +0100
@@ -17,6 +17,10 @@
 declare [[sledgehammer_instantiate_inducts]]
 
 ML {*
+! Multithreading.max_threads
+*}
+
+ML {*
 open MaSh_Eval
 *}
 

--- a/src/HOL/TPTP/mash_eval.ML	Mon Dec 10 16:27:03 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Mon Dec 10 16:38:20 2012 +0100
@@ -21,7 +21,7 @@
 
 val MePoN = "MePo"
 val MaShN = "MaSh"
-val MeshN = "Mesh"
+val MeShN = "MeSh"
 val IsarN = "Isar"
 
 val all_names = map (rpair () o nickname_of) #> Symtab.make
@@ -112,9 +112,9 @@
         val [mepo_s, mash_s, mesh_s, isar_s] =
           [fn () => prove mepo_ok MePoN fst mepo_facts,
            fn () => prove mash_ok MaShN fst mash_facts,
-           fn () => prove mesh_ok MeshN I mesh_facts,
+           fn () => prove mesh_ok MeShN I mesh_facts,
            fn () => prove isar_ok IsarN fst isar_facts]
-          |> map (fn f => f ())
+          |> (* Par_List. *) map (fn f => f ())
       in
         ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
          isar_s]
@@ -134,11 +134,11 @@
   in
     print " * * *";
     print ("Options: " ^ commas options);
-    List.app solve_goal (tag_list 1 lines);
+    Par_List.map solve_goal (tag_list 1 lines);
     ["Successes (of " ^ string_of_int n ^ " goals)",
      total_of MePoN mepo_ok n,
      total_of MaShN mash_ok n,
-     total_of MeshN mesh_ok n,
+     total_of MeShN mesh_ok n,
      total_of IsarN isar_ok n]
     |> cat_lines |> print
   end