changeset 68803 | 169bf32b35dd |
parent 67147 | dea94b1aabc3 |
child 68812 | 10732941cc4b |
--- 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>