equal
deleted
inserted
replaced
3 Compatibility wrapper for Poly/ML 5.0. |
3 Compatibility wrapper for Poly/ML 5.0. |
4 *) |
4 *) |
5 |
5 |
6 use "ML-Systems/universal.ML"; |
6 use "ML-Systems/universal.ML"; |
7 use "ML-Systems/thread_dummy.ML"; |
7 use "ML-Systems/thread_dummy.ML"; |
|
8 use "ML-Systems/ml_name_space.ML"; |
8 use "ML-Systems/polyml_common.ML"; |
9 use "ML-Systems/polyml_common.ML"; |
9 use "ML-Systems/polyml_old_compiler5.ML"; |
10 use "ML-Systems/polyml_old_compiler5.ML"; |
10 use "ML-Systems/polyml_pp.ML"; |
11 use "ML-Systems/polyml_pp.ML"; |
11 |
12 |
12 val pointer_eq = PolyML.pointerEq; |
13 val pointer_eq = PolyML.pointerEq; |