merged

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Oct 27 09:24:45 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Oct 27 13:51:22 2009 +0100
@@ -271,7 +271,7 @@
                     Markup.markup Markup.sendback "apply metis")
                 | ERROR msg => (false, "Error: " ^ msg);
             val _ = unregister result (Thread.self ());
-          in () end handle Exn.Interrupt => ())
+          in () end)
       in () end);
 
 

--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Oct 27 09:24:45 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Oct 27 13:51:22 2009 +0100
@@ -432,7 +432,7 @@
     if auto orelse blocking then
       go ()
     else
-      (SimpleThread.fork true (fn () => (go (); ()) handle Exn.Interrupt => ());
+      (SimpleThread.fork true (fn () => (go (); ()));
        state)
   end
 

--- a/src/Pure/Concurrent/simple_thread.ML	Tue Oct 27 09:24:45 2009 +0100
+++ b/src/Pure/Concurrent/simple_thread.ML	Tue Oct 27 13:51:22 2009 +0100
@@ -15,7 +15,7 @@
 struct
 
 fun fork interrupts body =
-  Thread.fork (fn () => exception_trace (fn () => body ()),
+  Thread.fork (fn () => exception_trace (fn () => body () handle Exn.Interrupt => ()),
     if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
 
 fun interrupt thread = Thread.interrupt thread handle Thread _ => ();

--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Oct 27 09:24:45 2009 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Oct 27 13:51:22 2009 +0100
@@ -33,14 +33,9 @@
 
 val max_threads = Unsynchronized.ref 0;
 
-val tested_platform =
-  let val ml_platform = getenv "ML_PLATFORM"
-  in String.isSuffix "linux" ml_platform orelse String.isSuffix "darwin" ml_platform end;
-
 fun max_threads_value () =
   let val m = ! max_threads in
     if m > 0 then m
-    else if not tested_platform then 1
     else Int.min (Int.max (Thread.numProcessors (), 1), 4)
   end;