removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1);
authorwenzelm
Mon Mar 24 18:35:41 2008 +0100 (2008-03-24 ago)
changeset 2637754dc2f9c5be8
parent 26376 1aeabd85866a
child 26378 bac8d5e5f833
removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1);
src/Pure/ML-Systems/polyml-4.1.3.ML
src/Pure/ML-Systems/polyml-4.1.4.ML
src/Pure/ML-Systems/polyml-4.2.0.ML
     1.1 --- a/src/Pure/ML-Systems/polyml-4.1.3.ML	Mon Mar 24 18:35:40 2008 +0100
     1.2 +++ b/src/Pure/ML-Systems/polyml-4.1.3.ML	Mon Mar 24 18:35:41 2008 +0100
     1.3 @@ -6,3 +6,7 @@
     1.4  
     1.5  use "ML-Systems/polyml_old_basis.ML";
     1.6  use "ML-Systems/polyml_common.ML";
     1.7 +use "ML-Systems/polyml_old_compiler4.ML";
     1.8 +
     1.9 +val pointer_eq = Address.wordEq;
    1.10 +
     2.1 --- a/src/Pure/ML-Systems/polyml-4.1.4.ML	Mon Mar 24 18:35:40 2008 +0100
     2.2 +++ b/src/Pure/ML-Systems/polyml-4.1.4.ML	Mon Mar 24 18:35:41 2008 +0100
     2.3 @@ -6,3 +6,7 @@
     2.4  
     2.5  use "ML-Systems/polyml_old_basis.ML";
     2.6  use "ML-Systems/polyml_common.ML";
     2.7 +use "ML-Systems/polyml_old_compiler4.ML";
     2.8 +
     2.9 +val pointer_eq = Address.wordEq;
    2.10 +
     3.1 --- a/src/Pure/ML-Systems/polyml-4.2.0.ML	Mon Mar 24 18:35:40 2008 +0100
     3.2 +++ b/src/Pure/ML-Systems/polyml-4.2.0.ML	Mon Mar 24 18:35:41 2008 +0100
     3.3 @@ -5,3 +5,7 @@
     3.4  *)
     3.5  
     3.6  use "ML-Systems/polyml_common.ML";
     3.7 +use "ML-Systems/polyml_old_compiler4.ML";
     3.8 +
     3.9 +val pointer_eq = Address.wordEq;
    3.10 +