equal
deleted
inserted
replaced
1 (* Title: Pure/ML-Systems/polyml-5.1.ML |
1 (* Title: Pure/ML-Systems/polyml-5.1.ML |
2 |
2 |
3 Compatibility wrapper for Poly/ML 5.1. |
3 Compatibility wrapper for Poly/ML 5.1. |
4 *) |
4 *) |
|
5 |
|
6 fun reraise exn = raise exn; |
5 |
7 |
6 use "ML-Systems/thread_dummy.ML"; |
8 use "ML-Systems/thread_dummy.ML"; |
7 use "ML-Systems/ml_name_space.ML"; |
9 use "ML-Systems/ml_name_space.ML"; |
8 use "ML-Systems/polyml_common.ML"; |
10 use "ML-Systems/polyml_common.ML"; |
9 use "ML-Systems/compiler_polyml-5.0.ML"; |
11 use "ML-Systems/compiler_polyml-5.0.ML"; |