tuned;
authorwenzelm
Sat, 02 Apr 2016 22:13:00 +0200
changeset 62822 941b6a48ff67
parent 62821 48c24d0b6d85
child 62823 751bcf0473a7
tuned;
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;