changeset 28836 | dd361ca41f69 |
parent 28254 | d67ba23e0277 |
child 29564 | f8b933a62151 |
28835:d4d8eba5f781 | 28836:dd361ca41f69 |
---|---|
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 open Thread; |
7 use "ML-Systems/thread_dummy.ML"; |
8 use "ML-Systems/polyml_common.ML"; |
8 use "ML-Systems/polyml_common.ML"; |
9 use "ML-Systems/polyml_old_compiler5.ML"; |
9 use "ML-Systems/polyml_old_compiler5.ML"; |
10 |
10 |
11 val pointer_eq = PolyML.pointerEq; |
11 val pointer_eq = PolyML.pointerEq; |