# HG changeset patch
# User blanchet
# Date 1284540237 -7200
# Node ID 0049301f7333027d235abcef53eb9ba6fcf1384e
# Parent  76603e40bd4cf490979d802b26623b0502eeda9b
compile on SML/NJ

diff -r 76603e40bd4c -r 0049301f7333 src/Tools/Metis/metis.ML
--- a/src/Tools/Metis/metis.ML	Wed Sep 15 10:26:09 2010 +0200
+++ b/src/Tools/Metis/metis.ML	Wed Sep 15 10:43:57 2010 +0200
@@ -179,7 +179,7 @@
 (* Pointer equality using the run-time system.                               *)
 (* ------------------------------------------------------------------------- *)
 
-fun pointerEqual (x : 'a, y : 'a) = PolyML.pointerEq(x,y);
+fun pointerEqual (x : 'a, y : 'a) = pointer_eq (x, y) (* MODIFIED by Jasmin Blanchette *)
 
 (* ------------------------------------------------------------------------- *)
 (* Timing function applications.                                             *)