equal
deleted
inserted
replaced
4 Compatibility wrapper for Poly/ML 5.2 or later. |
4 Compatibility wrapper for Poly/ML 5.2 or later. |
5 *) |
5 *) |
6 |
6 |
7 open Thread; |
7 open Thread; |
8 use "ML-Systems/polyml_common.ML"; |
8 use "ML-Systems/polyml_common.ML"; |
9 use "ML-Systems/multithreading_polyml.ML"; |
9 |
|
10 if ml_system = "polyml-5.2" then () |
|
11 else use "ML-Systems/multithreading_polyml.ML"; |
10 |
12 |
11 val pointer_eq = PolyML.pointerEq; |
13 val pointer_eq = PolyML.pointerEq; |
12 |
14 |
13 |
15 |
14 (* runtime compilation *) |
16 (* runtime compilation *) |