# HG changeset patch
# User wenzelm
# Date 1206380141 -3600
# Node ID 54dc2f9c5be8880e4a9b1cf6617f193a586c61b6
# Parent  1aeabd85866a362404dbd59c18c0c224f6e3f3cb
removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1);

diff -r 1aeabd85866a -r 54dc2f9c5be8 src/Pure/ML-Systems/polyml-4.1.3.ML
--- a/src/Pure/ML-Systems/polyml-4.1.3.ML	Mon Mar 24 18:35:40 2008 +0100
+++ b/src/Pure/ML-Systems/polyml-4.1.3.ML	Mon Mar 24 18:35:41 2008 +0100
@@ -6,3 +6,7 @@
 
 use "ML-Systems/polyml_old_basis.ML";
 use "ML-Systems/polyml_common.ML";
+use "ML-Systems/polyml_old_compiler4.ML";
+
+val pointer_eq = Address.wordEq;
+
diff -r 1aeabd85866a -r 54dc2f9c5be8 src/Pure/ML-Systems/polyml-4.1.4.ML
--- a/src/Pure/ML-Systems/polyml-4.1.4.ML	Mon Mar 24 18:35:40 2008 +0100
+++ b/src/Pure/ML-Systems/polyml-4.1.4.ML	Mon Mar 24 18:35:41 2008 +0100
@@ -6,3 +6,7 @@
 
 use "ML-Systems/polyml_old_basis.ML";
 use "ML-Systems/polyml_common.ML";
+use "ML-Systems/polyml_old_compiler4.ML";
+
+val pointer_eq = Address.wordEq;
+
diff -r 1aeabd85866a -r 54dc2f9c5be8 src/Pure/ML-Systems/polyml-4.2.0.ML
--- a/src/Pure/ML-Systems/polyml-4.2.0.ML	Mon Mar 24 18:35:40 2008 +0100
+++ b/src/Pure/ML-Systems/polyml-4.2.0.ML	Mon Mar 24 18:35:41 2008 +0100
@@ -5,3 +5,7 @@
 *)
 
 use "ML-Systems/polyml_common.ML";
+use "ML-Systems/polyml_old_compiler4.ML";
+
+val pointer_eq = Address.wordEq;
+