equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 |
3 |
4 Compatibility wrapper for Poly/ML 5.1. |
4 Compatibility wrapper for Poly/ML 5.1. |
5 *) |
5 *) |
6 |
6 |
|
7 structure PolyML_Thread = Thread; |
7 use "ML-Systems/polyml_common.ML"; |
8 use "ML-Systems/polyml_common.ML"; |
|
9 |
|
10 open PolyML_Thread; |
8 use "ML-Systems/multithreading_polyml.ML"; |
11 use "ML-Systems/multithreading_polyml.ML"; |
|
12 |
9 use "ML-Systems/polyml_old_compiler5.ML"; |
13 use "ML-Systems/polyml_old_compiler5.ML"; |
10 |
14 |
11 val pointer_eq = PolyML.pointerEq; |
15 val pointer_eq = PolyML.pointerEq; |
12 |
16 |