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;