removed share_data;
tuned;

--- 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;