avoid creating nested threads for MaSh -- this seems to cause thread creation failures for machines with dozens of cores (unclear yet if that's really the issue)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Dec 15 19:57:12 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Dec 15 21:26:10 2012 +0100
@@ -746,7 +746,8 @@
                 |> seconds |> SOME
               | NONE => NONE
             val generous_slice_timeout =
-              Option.map (curry Time.+ atp_timeout_slack) slice_timeout
+              if mode = MaSh then NONE
+              else Option.map (curry Time.+ atp_timeout_slack) slice_timeout
             val _ =
               if debug then
                 quote name ^ " slice #" ^ string_of_int (slice + 1) ^