| changeset 30627 | fb9e73c01603 |
| parent 29564 | f8b933a62151 |
| child 30672 | beaadd5af500 |
| 30626:248de8dd839e | 30627:fb9e73c01603 |
|---|---|
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/polyml_common.ML"; |
8 use "ML-Systems/polyml_common.ML"; |
9 use "ML-Systems/polyml_old_compiler4.ML"; |
9 use "ML-Systems/polyml_old_compiler4.ML"; |
10 use "ML-Systems/polyml_pp.ML"; |
|
10 |
11 |
11 val pointer_eq = Address.wordEq; |
12 val pointer_eq = Address.wordEq; |
12 |
13 |