# HG changeset patch
# User wenzelm
# Date 1535185771 -7200
# Node ID 169bf32b35dd1a107f78bf97473d7b236a55b4c6
# Parent  3974935e0252d0bf411d5f9d7bc960218025706a
retain original PolyML.pointerEq;

diff -r 3974935e0252 -r 169bf32b35dd NEWS
--- 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)
 ---------------------------------
 
diff -r 3974935e0252 -r 169bf32b35dd src/Pure/ML_Bootstrap.thy
--- 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>