# HG changeset patch
# User blanchet
# Date 1355603170 -3600
# Node ID a719106124d806bfca71a056758e8af1e7c77257
# Parent  31313171deb5be0da7116be5fd56fe85adb1ed71
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)

diff -r 31313171deb5 -r a719106124d8 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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) ^