tuned;
authorwenzelm
Sat Apr 02 22:13:00 2016 +0200 (2016-04-02 ago)
changeset 62822941b6a48ff67
parent 62821 48c24d0b6d85
child 62823 751bcf0473a7
tuned;
src/Pure/ML/ml_debugger.ML
     1.1 --- a/src/Pure/ML/ml_debugger.ML	Sat Apr 02 21:55:32 2016 +0200
     1.2 +++ b/src/Pure/ML/ml_debugger.ML	Sat Apr 02 22:13:00 2016 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4    Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0));
     1.5  
     1.6  fun print_exn_id (Exn_Id (name, _)) = name;
     1.7 -fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2);
     1.8 +fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = pointer_eq (id1, id2);
     1.9  
    1.10  end;
    1.11