# HG changeset patch
# User bulwahn
# Date 1256647882 -3600
# Node ID 2ac8ef0342b470fac4851f28dd38d39ce032615c
# Parent  f47ca46d2187cf44ab510c7046065404c896dc90# Parent  11a1af478dac0fd69ad00ba672de0ed977c83524
merged

diff -r f47ca46d2187 -r 2ac8ef0342b4 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- 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);
 
 
diff -r f47ca46d2187 -r 2ac8ef0342b4 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- 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
 
diff -r f47ca46d2187 -r 2ac8ef0342b4 src/Pure/Concurrent/simple_thread.ML
--- 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 _ => ();
diff -r f47ca46d2187 -r 2ac8ef0342b4 src/Pure/ML-Systems/multithreading_polyml.ML
--- 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;