| changeset 28152 | c1277547d59f |
| parent 28125 | e99427bcf7f3 |
| child 28153 | 67147cc3f967 |
--- a/src/Pure/ML-Systems/polyml.ML Sun Sep 07 17:46:43 2008 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Sun Sep 07 17:46:44 2008 +0200 @@ -4,10 +4,8 @@ Compatibility wrapper for Poly/ML (after 5.1). *) -structure PolyML_Thread = Thread; +open Thread; use "ML-Systems/polyml_common.ML"; - -open PolyML_Thread; use "ML-Systems/multithreading_polyml.ML"; val pointer_eq = PolyML.pointerEq;