src/Pure/ML-Systems/polyml-4.2.0.ML
author haftmann
Wed, 11 Mar 2009 08:45:57 +0100
changeset 30432 aad3cd70e25a
parent 29564 f8b933a62151
child 30627 fb9e73c01603
permissions -rw-r--r--
merged
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26215
94d32a7cd0fb rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/polyml-4.2.0.ML
94d32a7cd0fb rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff changeset
     2
94d32a7cd0fb rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff changeset
     3
Compatibility wrapper for Poly/ML 4.2.0.
94d32a7cd0fb rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff changeset
     4
*)
94d32a7cd0fb rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff changeset
     5
28151
61f9c918b410 explicit use of universal.ML and dummy_thread.ML;
wenzelm
parents: 26377
diff changeset
     6
use "ML-Systems/universal.ML";
61f9c918b410 explicit use of universal.ML and dummy_thread.ML;
wenzelm
parents: 26377
diff changeset
     7
use "ML-Systems/thread_dummy.ML";
26215
94d32a7cd0fb rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff changeset
     8
use "ML-Systems/polyml_common.ML";
26377
54dc2f9c5be8 removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1);
wenzelm
parents: 26215
diff changeset
     9
use "ML-Systems/polyml_old_compiler4.ML";
54dc2f9c5be8 removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1);
wenzelm
parents: 26215
diff changeset
    10
54dc2f9c5be8 removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1);
wenzelm
parents: 26215
diff changeset
    11
val pointer_eq = Address.wordEq;
54dc2f9c5be8 removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1);
wenzelm
parents: 26215
diff changeset
    12