# HG changeset patch
# User wenzelm
# Date 1386852644 -3600
# Node ID 124432e77ecfc4006a7673e93e7cdf5ff234efed
# Parent  5f5608bfe2307619ba4e299f8766ecfe1d6765ea
simplified polyml-5.5.2 setup -- implicit upgrade of Thread.numProcessors;

diff -r 5f5608bfe230 -r 124432e77ecf src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Dec 12 13:23:23 2013 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Dec 12 13:50:44 2013 +0100
@@ -81,12 +81,7 @@
 
 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;
+  else Int.min (Int.max (Thread.numProcessors (), 1), 8);
 
 val max_threads = ref 1;
 
diff -r 5f5608bfe230 -r 124432e77ecf src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Thu Dec 12 13:23:23 2013 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Dec 12 13:50:44 2013 +0100
@@ -44,9 +44,6 @@
 else use "ML-Systems/single_assignment_polyml.ML";
 
 open Thread;
-if ML_System.name = "polyml-5.5.2" then ()
-else use "ML-Systems/thread_physical_processors.ML";
-
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/multithreading_polyml.ML";
 
diff -r 5f5608bfe230 -r 124432e77ecf src/Pure/ML-Systems/thread_physical_processors.ML
--- a/src/Pure/ML-Systems/thread_physical_processors.ML	Thu Dec 12 13:23:23 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-(*  Title:      Pure/ML-Systems/thread_physical_processors.ML
-    Author:     Makarius
-
-Emulation of structure Thread in Poly/ML 5.5.2 (SVN 1890).
-*)
-
-structure Thread =
-struct
-  open Thread;
-
-  fun numPhysicalProcessors () : int option = NONE;
-end;
diff -r 5f5608bfe230 -r 124432e77ecf src/Pure/ROOT
--- a/src/Pure/ROOT	Thu Dec 12 13:23:23 2013 +0100
+++ b/src/Pure/ROOT	Thu Dec 12 13:50:44 2013 +0100
@@ -12,6 +12,7 @@
     "ML-Systems/multithreading_polyml.ML"
     "ML-Systems/overloading_smlnj.ML"
     "ML-Systems/polyml.ML"
+    "ML-Systems/polyml-5.5.2.ML"
     "ML-Systems/pp_dummy.ML"
     "ML-Systems/proper_int.ML"
     "ML-Systems/single_assignment.ML"
@@ -19,7 +20,6 @@
     "ML-Systems/share_common_data_polyml-5.3.0.ML"
     "ML-Systems/smlnj.ML"
     "ML-Systems/thread_dummy.ML"
-    "ML-Systems/thread_physical_processors.ML"
     "ML-Systems/universal.ML"
     "ML-Systems/unsynchronized.ML"
     "ML-Systems/use_context.ML"
@@ -36,13 +36,13 @@
     "ML-Systems/multithreading_polyml.ML"
     "ML-Systems/overloading_smlnj.ML"
     "ML-Systems/polyml.ML"
+    "ML-Systems/polyml-5.5.2.ML"
     "ML-Systems/pp_dummy.ML"
     "ML-Systems/proper_int.ML"
     "ML-Systems/single_assignment.ML"
     "ML-Systems/single_assignment_polyml.ML"
     "ML-Systems/smlnj.ML"
     "ML-Systems/thread_dummy.ML"
-    "ML-Systems/thread_physical_processors.ML"
     "ML-Systems/universal.ML"
     "ML-Systems/unsynchronized.ML"
     "ML-Systems/use_context.ML"