retain original PolyML.pointerEq;

--- a/NEWS	Fri Aug 24 20:22:14 2018 +0000
+++ b/NEWS	Sat Aug 25 10:29:31 2018 +0200
@@ -23,6 +23,13 @@
 retained as migration auxiliary. INCOMPATIBILITY.
 
 
+*** ML ***
+
+* Original PolyML.pointerEq is retained as a convenience for tools that
+don't use Isabelle/ML (where this is called "pointer_eq").
+
+
+
 New in Isabelle2018 (August 2018)
 ---------------------------------
 

--- a/src/Pure/ML_Bootstrap.thy	Fri Aug 24 20:22:14 2018 +0000
+++ b/src/Pure/ML_Bootstrap.thy	Sat Aug 25 10:29:31 2018 +0200
@@ -30,7 +30,11 @@
   Context.setmp_generic_context NONE
     ML \<open>
       List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
-      structure PolyML = struct structure IntInf = PolyML.IntInf end;
+      structure PolyML =
+      struct
+        val pointerEq = pointer_eq;
+        structure IntInf = PolyML.IntInf;
+      end;
     \<close>
 \<close>