# HG changeset patch
# User wenzelm
# Date 1119372944 -7200
# Node ID 0842635545c3212d323a73c6205176c3cf191e84
# Parent  7896ea4f3a87ef473d3626a74a1460a38f51aac8
tuned pointer_eq;

diff -r 7896ea4f3a87 -r 0842635545c3 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Tue Jun 21 13:34:24 2005 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Jun 21 18:55:44 2005 +0200
@@ -21,9 +21,8 @@
 fun unless_cygwin f x = if not cygwin_platform then f x else ();
 
 
-(* low-level pointer equality *)
-
-fun pointer_eq (x:''a, y) = Address.wordEq (x, y);
+(*low-level pointer equality*)
+val pointer_eq = Address.wordEq;
 
 
 (* old Poly/ML emulation *)