changeset 26377 | 54dc2f9c5be8 |
parent 26215 | 94d32a7cd0fb |
child 28151 | 61f9c918b410 |
26376:1aeabd85866a | 26377:54dc2f9c5be8 |
---|---|
4 Compatibility wrapper for Poly/ML 4.1.3. |
4 Compatibility wrapper for Poly/ML 4.1.3. |
5 *) |
5 *) |
6 |
6 |
7 use "ML-Systems/polyml_old_basis.ML"; |
7 use "ML-Systems/polyml_old_basis.ML"; |
8 use "ML-Systems/polyml_common.ML"; |
8 use "ML-Systems/polyml_common.ML"; |
9 use "ML-Systems/polyml_old_compiler4.ML"; |
|
10 |
|
11 val pointer_eq = Address.wordEq; |
|
12 |