author | wenzelm |
Thu, 04 Sep 2008 16:03:48 +0200 | |
changeset 28125 | e99427bcf7f3 |
parent 28124 | 10a1f1f4c6ae |
child 28126 | 7332b623b569 |
--- a/src/Pure/ML-Systems/polyml.ML Thu Sep 04 16:03:47 2008 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Thu Sep 04 16:03:48 2008 +0200 @@ -4,7 +4,10 @@ Compatibility wrapper for Poly/ML (after 5.1). *) +structure PolyML_Thread = Thread; use "ML-Systems/polyml_common.ML"; + +open PolyML_Thread; use "ML-Systems/multithreading_polyml.ML"; val pointer_eq = PolyML.pointerEq;