simplified signature (again, see 751bcf0473a7): e.g. relevant for non-Isabelle ML environments;

--- a/src/Pure/Concurrent/future.ML	Thu Sep 06 13:54:07 2018 +0200
+++ b/src/Pure/Concurrent/future.ML	Thu Sep 06 14:08:35 2018 +0200
@@ -112,8 +112,8 @@
 val _ =
   ML_system_pp (fn depth => fn pretty => fn x =>
     (case peek x of
-      NONE => PolyML_Pretty.PrettyString "<future>"
-    | SOME (Exn.Exn _) => PolyML_Pretty.PrettyString "<failed>"
+      NONE => PolyML.PrettyString "<future>"
+    | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
     | SOME (Exn.Res y) => pretty (y, depth)));
 
 

--- a/src/Pure/Concurrent/lazy.ML	Thu Sep 06 13:54:07 2018 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Thu Sep 06 14:08:35 2018 +0200
@@ -157,8 +157,8 @@
 val _ =
   ML_system_pp (fn depth => fn pretty => fn x =>
     (case peek x of
-      NONE => PolyML_Pretty.PrettyString "<lazy>"
-    | SOME (Exn.Exn _) => PolyML_Pretty.PrettyString "<failed>"
+      NONE => PolyML.PrettyString "<lazy>"
+    | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
     | SOME (Exn.Res y) => pretty (y, depth)));
 
 end;

--- a/src/Pure/General/pretty.ML	Thu Sep 06 13:54:07 2018 +0200
+++ b/src/Pure/General/pretty.ML	Thu Sep 06 14:08:35 2018 +0200
@@ -76,8 +76,8 @@
   val writeln_chunks2: T list -> unit
   val to_ML: FixedInt.int -> T -> ML_Pretty.pretty
   val from_ML: ML_Pretty.pretty -> T
-  val to_polyml: T -> PolyML_Pretty.pretty
-  val from_polyml: PolyML_Pretty.pretty -> T
+  val to_polyml: T -> PolyML.pretty
+  val from_polyml: PolyML.pretty -> T
 end;
 
 structure Pretty: PRETTY =

--- a/src/Pure/ML/ml_init.ML	Thu Sep 06 13:54:07 2018 +0200
+++ b/src/Pure/ML/ml_init.ML	Thu Sep 06 14:08:35 2018 +0200
@@ -4,12 +4,6 @@
 Initial ML environment.
 *)
 
-structure PolyML_Pretty =
-struct
-  datatype context = datatype PolyML.context;
-  datatype pretty = datatype PolyML.pretty;
-end;
-
 val seconds = Time.fromReal;
 
 val _ =

--- a/src/Pure/ML/ml_pretty.ML	Thu Sep 06 13:54:07 2018 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Thu Sep 06 14:08:35 2018 +0200
@@ -17,12 +17,12 @@
     ('a * 'b) * FixedInt.int -> pretty
   val enum: string -> string -> string -> ('a * FixedInt.int -> pretty) ->
     'a list * FixedInt.int -> pretty
-  val to_polyml: pretty -> PolyML_Pretty.pretty
-  val from_polyml: PolyML_Pretty.pretty -> pretty
-  val format_polyml: int -> PolyML_Pretty.pretty -> string
+  val to_polyml: pretty -> PolyML.pretty
+  val from_polyml: PolyML.pretty -> pretty
+  val format_polyml: int -> PolyML.pretty -> string
   val format: int -> pretty -> string
   val default_margin: int
-  val string_of_polyml: PolyML_Pretty.pretty -> string
+  val string_of_polyml: PolyML.pretty -> string
   val make_string_fn: string
 end;
 
@@ -54,39 +54,39 @@
 
 (* convert *)
 
-fun to_polyml (Break (false, width, offset)) = PolyML_Pretty.PrettyBreak (width, offset)
+fun to_polyml (Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
   | to_polyml (Break (true, _, _)) =
-      PolyML_Pretty.PrettyBlock (0, false, [PolyML_Pretty.ContextProperty ("fbrk", "")],
-        [PolyML_Pretty.PrettyString " "])
+      PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
+        [PolyML.PrettyString " "])
   | to_polyml (Block ((bg, en), consistent, ind, prts)) =
       let val context =
-        (if bg = "" then [] else [PolyML_Pretty.ContextProperty ("begin", bg)]) @
-        (if en = "" then [] else [PolyML_Pretty.ContextProperty ("end", en)])
-      in PolyML_Pretty.PrettyBlock (ind, consistent, context, map to_polyml prts) end
+        (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
+        (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
+      in PolyML.PrettyBlock (ind, consistent, context, map to_polyml prts) end
   | to_polyml (String (s, len)) =
-      if len = FixedInt.fromInt (size s) then PolyML_Pretty.PrettyString s
+      if len = FixedInt.fromInt (size s) then PolyML.PrettyString s
       else
-        PolyML_Pretty.PrettyBlock
+        PolyML.PrettyBlock
           (0, false,
-            [PolyML_Pretty.ContextProperty ("length", FixedInt.toString len)], [PolyML_Pretty.PrettyString s]);
+            [PolyML.ContextProperty ("length", FixedInt.toString len)], [PolyML.PrettyString s]);
 
 val from_polyml =
   let
-    fun convert _ (PolyML_Pretty.PrettyBreak (width, offset)) = Break (false, width, offset)
-      | convert _ (PolyML_Pretty.PrettyBlock (_, _,
-            [PolyML_Pretty.ContextProperty ("fbrk", _)], [PolyML_Pretty.PrettyString " "])) =
+    fun convert _ (PolyML.PrettyBreak (width, offset)) = Break (false, width, offset)
+      | convert _ (PolyML.PrettyBlock (_, _,
+            [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
           Break (true, 1, 0)
-      | convert len (PolyML_Pretty.PrettyBlock (ind, consistent, context, prts)) =
+      | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) =
           let
             fun property name default =
-              (case List.find (fn PolyML_Pretty.ContextProperty (a, _) => name = a | _ => false) context of
-                SOME (PolyML_Pretty.ContextProperty (_, b)) => b
+              (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
+                SOME (PolyML.ContextProperty (_, b)) => b
               | _ => default);
             val bg = property "begin" "";
             val en = property "end" "";
             val len' = property "length" len;
           in Block ((bg, en), consistent, ind, map (convert len') prts) end
-      | convert len (PolyML_Pretty.PrettyString s) =
+      | convert len (PolyML.PrettyString s) =
           String (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
   in convert "" end;
 

--- 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>