equal
deleted
inserted
replaced
19 |
19 |
20 fun if_cygwin f x = if cygwin_platform then f x else (); |
20 fun if_cygwin f x = if cygwin_platform then f x else (); |
21 fun unless_cygwin f x = if not cygwin_platform then f x else (); |
21 fun unless_cygwin f x = if not cygwin_platform then f x else (); |
22 |
22 |
23 |
23 |
24 (* low-level pointer equality *) |
24 (*low-level pointer equality*) |
25 |
25 val pointer_eq = Address.wordEq; |
26 fun pointer_eq (x:''a, y) = Address.wordEq (x, y); |
|
27 |
26 |
28 |
27 |
29 (* old Poly/ML emulation *) |
28 (* old Poly/ML emulation *) |
30 |
29 |
31 local |
30 local |