author | wenzelm |
Sat, 22 Feb 2014 15:07:33 +0100 | |
changeset 55666 | cc350eb1087e |
parent 54726 | 5285805af26c |
permissions | -rw-r--r-- |
54726 | 1 |
(* Title: Pure/ML-Systems/polyml-5.5.2.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Compatibility wrapper for Poly/ML 5.5.2. |
|
5 |
*) |
|
6 |
||
7 |
structure Thread = |
|
8 |
struct |
|
9 |
open Thread; |
|
10 |
||
11 |
structure Thread = |
|
12 |
struct |
|
13 |
open Thread; |
|
14 |
||
15 |
fun numProcessors () = |
|
16 |
(case Thread.numPhysicalProcessors () of |
|
17 |
SOME n => n |
|
18 |
| NONE => Thread.numProcessors ()); |
|
19 |
end; |
|
20 |
end; |
|
21 |
||
22 |
use "ML-Systems/polyml.ML"; |
|
23 |