| changeset 62512 | 922e702ae8ca |
| parent 62500 | ff99681b3fd8 |
| parent 62511 | 93fa1efc7219 |
| child 62513 | 702085ca8564 |
| 62500:ff99681b3fd8 | 62512:922e702ae8ca |
|---|---|
1 (* Title: Pure/RAW/ROOT_polyml-5.6.ML |
|
2 Author: Makarius |
|
3 |
|
4 Compatibility wrapper for Poly/ML 5.6. |
|
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 "RAW/ROOT_polyml.ML"; |