src/Pure/ML-Systems/polyml.ML

   let val n = size ml_platform
   in n >= 6 andalso String.substring (ml_platform, n - 6, 6) = "cygwin" end;
 
 fun if_cygwin f x = if cygwin_platform then f x else ();
 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);
 
 
 (* old Poly/ML emulation *)
 
 local