src/Pure/ML-Systems/polyml-5.0.ML
changeset 30672 beaadd5af500
parent 30627 fb9e73c01603
child 31312 1c00e4ff3c99
equal deleted inserted replaced
30671:2f64540707d6 30672:beaadd5af500
     3 Compatibility wrapper for Poly/ML 5.0.
     3 Compatibility wrapper for Poly/ML 5.0.
     4 *)
     4 *)
     5 
     5 
     6 use "ML-Systems/universal.ML";
     6 use "ML-Systems/universal.ML";
     7 use "ML-Systems/thread_dummy.ML";
     7 use "ML-Systems/thread_dummy.ML";
       
     8 use "ML-Systems/ml_name_space.ML";
     8 use "ML-Systems/polyml_common.ML";
     9 use "ML-Systems/polyml_common.ML";
     9 use "ML-Systems/polyml_old_compiler5.ML";
    10 use "ML-Systems/polyml_old_compiler5.ML";
    10 use "ML-Systems/polyml_pp.ML";
    11 use "ML-Systems/polyml_pp.ML";
    11 
    12 
    12 val pointer_eq = PolyML.pointerEq;
    13 val pointer_eq = PolyML.pointerEq;