diff -r 6666fc0b9ebc -r 42c209a6c225 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Dec 11 00:17:09 2013 +0000
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Dec 11 18:02:22 2013 +0100
@@ -25,21 +25,6 @@
 structure Multithreading: MULTITHREADING =
 struct
 
-(* options *)
-
-val available = true;
-
-val max_threads = ref 1;
-
-fun max_threads_value () =
-  let val m = ! max_threads in
-    if m > 0 then m
-    else Int.min (Int.max (Thread.numProcessors (), 1), 8)
-  end;
-
-fun enabled () = max_threads_value () > 1;
-
-
 (* thread attributes *)
 
 val no_interrupts =
@@ -90,6 +75,37 @@
     f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
 
 
+(* options *)
+
+val available = true;
+
+fun max_threads_result m =
+  if m > 0 then m
+  else
+    let val n =
+      (case Thread.numPhysicalProcessors () of
+        SOME n => n
+      | NONE => Thread.numProcessors ())
+    in Int.min (Int.max (n, 1), 8) end;
+
+val max_threads = ref 1;
+
+fun max_threads_value () = ! max_threads;
+
+fun max_threads_update m = max_threads := max_threads_result m;
+
+fun max_threads_setmp m f x =
+  uninterruptible (fn restore_attributes => fn () =>
+    let
+      val max_threads_orig = ! max_threads;
+      val _ = max_threads_update m;
+      val result = Exn.capture (restore_attributes f) x;
+      val _ = max_threads := max_threads_orig;
+    in Exn.release result end) ();
+
+fun enabled () = max_threads_value () > 1;
+
+
 (* synchronous wait *)
 
 fun sync_wait opt_atts time cond lock =