multithreading.ML provides dummy thread structures;
authorwenzelm
Fri Sep 05 11:50:35 2008 +0200 (2008-09-05)
changeset 281442c27248bf267
parent 28143 e5c6c4aac52c
child 28145 af3923ed4786
multithreading.ML provides dummy thread structures;
src/Pure/ML-Systems/polyml-5.1.ML
     1.1 --- a/src/Pure/ML-Systems/polyml-5.1.ML	Fri Sep 05 06:50:22 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/polyml-5.1.ML	Fri Sep 05 11:50:35 2008 +0200
     1.3 @@ -4,8 +4,12 @@
     1.4  Compatibility wrapper for Poly/ML 5.1.
     1.5  *)
     1.6  
     1.7 +structure PolyML_Thread = Thread;
     1.8  use "ML-Systems/polyml_common.ML";
     1.9 +
    1.10 +open PolyML_Thread;
    1.11  use "ML-Systems/multithreading_polyml.ML";
    1.12 +
    1.13  use "ML-Systems/polyml_old_compiler5.ML";
    1.14  
    1.15  val pointer_eq = PolyML.pointerEq;