author | wenzelm |
Mon, 15 Feb 2016 14:55:44 +0100 | |
changeset 62337 | d3996d5873dd |
parent 62077 | e8ae72c26025 |
permissions | -rw-r--r-- |
62077 | 1 |
(* Title: Pure/RAW/ROOT_polyml-5.5.2.ML |
54726 | 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 |
||
62077 | 22 |
use "RAW/ROOT_polyml.ML"; |
54726 | 23 |