src/Pure/ML-Systems/polyml-4.9.1.ML
changeset 20816 1cf97e0bba57
parent 20779 4eb07237382a
child 21176 5ec545dbad6f
--- 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;