tuned pointer_eq;
authorwenzelm
Tue Jun 21 18:55:44 2005 +0200 (2005-06-21)
changeset 165160842635545c3
parent 16515 7896ea4f3a87
child 16517 4699288139f4
tuned pointer_eq;
src/Pure/ML-Systems/polyml.ML
     1.1 --- a/src/Pure/ML-Systems/polyml.ML	Tue Jun 21 13:34:24 2005 +0200
     1.2 +++ b/src/Pure/ML-Systems/polyml.ML	Tue Jun 21 18:55:44 2005 +0200
     1.3 @@ -21,9 +21,8 @@
     1.4  fun unless_cygwin f x = if not cygwin_platform then f x else ();
     1.5  
     1.6  
     1.7 -(* low-level pointer equality *)
     1.8 -
     1.9 -fun pointer_eq (x:''a, y) = Address.wordEq (x, y);
    1.10 +(*low-level pointer equality*)
    1.11 +val pointer_eq = Address.wordEq;
    1.12  
    1.13  
    1.14  (* old Poly/ML emulation *)