author | wenzelm |
Fri, 05 Sep 2008 11:50:35 +0200 | |
changeset 28144 | 2c27248bf267 |
parent 28143 | e5c6c4aac52c |
child 28145 | af3923ed4786 |
--- a/src/Pure/ML-Systems/polyml-5.1.ML Fri Sep 05 06:50:22 2008 +0200 +++ b/src/Pure/ML-Systems/polyml-5.1.ML Fri Sep 05 11:50:35 2008 +0200 @@ -4,8 +4,12 @@ Compatibility wrapper for Poly/ML 5.1. *) +structure PolyML_Thread = Thread; use "ML-Systems/polyml_common.ML"; + +open PolyML_Thread; use "ML-Systems/multithreading_polyml.ML"; + use "ML-Systems/polyml_old_compiler5.ML"; val pointer_eq = PolyML.pointerEq;