tuned pointer_eq;

--- 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 *)