retain original PolyML.pointerEq;
authorwenzelm
Sat Aug 25 10:29:31 2018 +0200 (15 months ago ago)
changeset 68804169bf32b35dd
parent 68802 3974935e0252
child 68805 cbde6e3b132b
retain original PolyML.pointerEq;
NEWS
src/Pure/ML_Bootstrap.thy
     1.1 --- a/NEWS	Fri Aug 24 20:22:14 2018 +0000
     1.2 +++ b/NEWS	Sat Aug 25 10:29:31 2018 +0200
     1.3 @@ -23,6 +23,13 @@
     1.4  retained as migration auxiliary. INCOMPATIBILITY.
     1.5  
     1.6  
     1.7 +*** ML ***
     1.8 +
     1.9 +* Original PolyML.pointerEq is retained as a convenience for tools that
    1.10 +don't use Isabelle/ML (where this is called "pointer_eq").
    1.11 +
    1.12 +
    1.13 +
    1.14  New in Isabelle2018 (August 2018)
    1.15  ---------------------------------
    1.16  
     2.1 --- a/src/Pure/ML_Bootstrap.thy	Fri Aug 24 20:22:14 2018 +0000
     2.2 +++ b/src/Pure/ML_Bootstrap.thy	Sat Aug 25 10:29:31 2018 +0200
     2.3 @@ -30,7 +30,11 @@
     2.4    Context.setmp_generic_context NONE
     2.5      ML \<open>
     2.6        List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
     2.7 -      structure PolyML = struct structure IntInf = PolyML.IntInf end;
     2.8 +      structure PolyML =
     2.9 +      struct
    2.10 +        val pointerEq = pointer_eq;
    2.11 +        structure IntInf = PolyML.IntInf;
    2.12 +      end;
    2.13      \<close>
    2.14  \<close>
    2.15