added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;

--- a/src/Pure/ML-Systems/multithreading.ML	Wed Jan 02 16:32:52 2008 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML	Wed Jan 02 16:32:53 2008 +0100
@@ -18,6 +18,7 @@
   val tracing: int -> (unit -> string) -> unit
   val available: bool
   val max_threads: int ref
+  val max_threads_value: unit -> int
   val self_critical: unit -> bool
   datatype 'a task =
     Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
@@ -37,6 +38,7 @@
 
 val available = false;
 val max_threads = ref (1: int);
+fun max_threads_value () = Int.max (! max_threads, 1);
 
 
 (* critical section *)

--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jan 02 16:32:52 2008 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jan 02 16:32:53 2008 +0100
@@ -38,8 +38,13 @@
   else ();
 
 val available = true;
+
 val max_threads = ref 1;
 
+fun max_threads_value () =
+  let val m = ! max_threads
+  in if m <= 0 then Thread.numProcessors () else m end;
+
 
 (* misc utils *)
 

--- a/src/Pure/Thy/thy_info.ML	Wed Jan 02 16:32:52 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML	Wed Jan 02 16:32:53 2008 +0100
@@ -377,7 +377,7 @@
 in
 
 fun schedule_tasks tasks n =
-  let val m = ! Multithreading.max_threads in
+  let val m = Multithreading.max_threads_value () in
     if m <= 1 orelse n <= 1 then schedule_seq tasks
     else if Multithreading.self_critical () then
      (warning (loader_msg "no multithreading within critical section" []);