src/Pure/ML_Bootstrap.thy
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>