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