src/Pure/ML-Systems/polyml.ML
changeset 16516 0842635545c3
parent 16502 5a56e59526a5
child 16659 1cf39eba29fe
     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 *)