# HG changeset patch
# User wenzelm
# Date 1459627980 -7200
# Node ID 941b6a48ff678874efb860da2fe2ac6c3194a852
# Parent  48c24d0b6d85012a29a15d328745a8091ac7b8d3
tuned;

diff -r 48c24d0b6d85 -r 941b6a48ff67 src/Pure/ML/ml_debugger.ML
--- a/src/Pure/ML/ml_debugger.ML	Sat Apr 02 21:55:32 2016 +0200
+++ b/src/Pure/ML/ml_debugger.ML	Sat Apr 02 22:13:00 2016 +0200
@@ -36,7 +36,7 @@
   Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0));
 
 fun print_exn_id (Exn_Id (name, _)) = name;
-fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2);
+fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = pointer_eq (id1, id2);
 
 end;