# HG changeset patch
# User wenzelm
# Date 1159720175 -7200
# Node ID 1cf97e0bba577021e40854b764d688d4dd3c486a
# Parent  ccf18b899c8d128f350a696ed1678cda7bcca8a9
removed share_data;
tuned;

diff -r ccf18b899c8d -r 1cf97e0bba57 src/Pure/ML-Systems/polyml-4.9.1.ML
--- a/src/Pure/ML-Systems/polyml-4.9.1.ML	Sun Oct 01 18:29:34 2006 +0200
+++ b/src/Pure/ML-Systems/polyml-4.9.1.ML	Sun Oct 01 18:29:35 2006 +0200
@@ -8,4 +8,4 @@
 use "ML-Systems/polyml-4.1.4-patch.ML";
 use "ML-Systems/polyml.ML";
 
-val share_data = SOME (fn x => (PolyML.shareCommonData x; x));
+val pointer_eq = PolyML.pointerEq;