author | wenzelm |
Sun, 01 Oct 2006 18:29:35 +0200 | |
changeset 20816 | 1cf97e0bba57 |
parent 20815 | ccf18b899c8d |
child 20817 | 7ec9b692183c |
--- 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;