equal
deleted
inserted
replaced
3 |
3 |
4 Compatibility wrapper for Poly/ML 4.1.4. |
4 Compatibility wrapper for Poly/ML 4.1.4. |
5 *) |
5 *) |
6 |
6 |
7 use "ML-Systems/polyml_old_basis.ML"; |
7 use "ML-Systems/polyml_old_basis.ML"; |
|
8 use "ML-Systems/universal.ML"; |
|
9 use "ML-Systems/thread_dummy.ML"; |
8 use "ML-Systems/polyml_common.ML"; |
10 use "ML-Systems/polyml_common.ML"; |
9 use "ML-Systems/polyml_old_compiler4.ML"; |
11 use "ML-Systems/polyml_old_compiler4.ML"; |
10 |
12 |
11 val pointer_eq = Address.wordEq; |
13 val pointer_eq = Address.wordEq; |
12 |
14 |