src/Pure/ML_Bootstrap.thy

--- a/src/Pure/ML_Bootstrap.thy	Thu Sep 06 13:54:07 2018 +0200
+++ b/src/Pure/ML_Bootstrap.thy	Thu Sep 06 14:08:35 2018 +0200
@@ -18,7 +18,7 @@
   structure Output_Primitives = Output_Primitives_Virtual;
   structure Thread_Data = Thread_Data_Virtual;
   structure PolyML = PolyML;
-  fun ML_system_pp (_: FixedInt.int -> 'a -> 'b -> PolyML_Pretty.pretty) = ();
+  fun ML_system_pp (_: FixedInt.int -> 'a -> 'b -> PolyML.pretty) = ();
 
   Proofterm.proofs := 0;
 
@@ -29,6 +29,8 @@
       struct
         val pointerEq = pointer_eq;
         structure IntInf = PolyML.IntInf;
+        datatype context = datatype PolyML.context;
+        datatype pretty = datatype PolyML.pretty;
       end;
     \<close>
 \<close>