tuned signature;

--- a/src/Pure/Concurrent/future.ML	Sat Apr 02 22:13:00 2016 +0200
+++ b/src/Pure/Concurrent/future.ML	Sat Apr 02 22:38:26 2016 +0200
@@ -102,8 +102,8 @@
 val _ =
   ML_system_pp (fn depth => fn pretty => fn x =>
     (case peek x of
-      NONE => PolyML.PrettyString "<future>"
-    | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
+      NONE => PolyML_Pretty.PrettyString "<future>"
+    | SOME (Exn.Exn _) => PolyML_Pretty.PrettyString "<failed>"
     | SOME (Exn.Res y) => pretty (y, depth)));
 
 

--- a/src/Pure/Concurrent/lazy.ML	Sat Apr 02 22:13:00 2016 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Sat Apr 02 22:38:26 2016 +0200
@@ -105,8 +105,8 @@
 val _ =
   ML_system_pp (fn depth => fn pretty => fn x =>
     (case peek x of
-      NONE => PolyML.PrettyString "<lazy>"
-    | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
+      NONE => PolyML_Pretty.PrettyString "<lazy>"
+    | SOME (Exn.Exn _) => PolyML_Pretty.PrettyString "<failed>"
     | SOME (Exn.Res y) => pretty (y, depth)));
 
 end;

--- a/src/Pure/General/pretty.ML	Sat Apr 02 22:13:00 2016 +0200
+++ b/src/Pure/General/pretty.ML	Sat Apr 02 22:38:26 2016 +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
-  val from_polyml: PolyML.pretty -> T
+  val to_polyml: T -> PolyML_Pretty.pretty
+  val from_polyml: PolyML_Pretty.pretty -> T
 end;
 
 structure Pretty: PRETTY =

--- a/src/Pure/ML/ml_pervasive.ML	Sat Apr 02 22:13:00 2016 +0200
+++ b/src/Pure/ML/ml_pervasive.ML	Sat Apr 02 22:38:26 2016 +0200
@@ -4,6 +4,12 @@
 Pervasive 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	Sat Apr 02 22:13:00 2016 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Sat Apr 02 22:38:26 2016 +0200
@@ -17,11 +17,11 @@
     ('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
-  val from_polyml: PolyML.pretty -> pretty
+  val to_polyml: pretty -> PolyML_Pretty.pretty
+  val from_polyml: PolyML_Pretty.pretty -> pretty
   val get_print_depth: unit -> int
   val print_depth: int -> unit
-  val format_polyml: int -> PolyML.pretty -> string
+  val format_polyml: int -> PolyML_Pretty.pretty -> string
   val format: int -> pretty -> string
   val make_string_fn: string -> string
 end;
@@ -54,39 +54,39 @@
 
 (* convert *)
 
-fun to_polyml (Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
+fun to_polyml (Break (false, width, offset)) = PolyML_Pretty.PrettyBreak (width, offset)
   | to_polyml (Break (true, _, _)) =
-      PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
-        [PolyML.PrettyString " "])
+      PolyML_Pretty.PrettyBlock (0, false, [PolyML_Pretty.ContextProperty ("fbrk", "")],
+        [PolyML_Pretty.PrettyString " "])
   | to_polyml (Block ((bg, en), consistent, ind, prts)) =
       let val context =
-        (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
+        (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
   | to_polyml (String (s, len)) =
-      if len = FixedInt.fromInt (size s) then PolyML.PrettyString s
+      if len = FixedInt.fromInt (size s) then PolyML_Pretty.PrettyString s
       else
-        PolyML.PrettyBlock
+        PolyML_Pretty.PrettyBlock
           (0, false,
-            [PolyML.ContextProperty ("length", FixedInt.toString len)], [PolyML.PrettyString s]);
+            [PolyML_Pretty.ContextProperty ("length", FixedInt.toString len)], [PolyML_Pretty.PrettyString s]);
 
 val from_polyml =
   let
-    fun convert _ (PolyML.PrettyBreak (width, offset)) = Break (false, width, offset)
-      | convert _ (PolyML.PrettyBlock (_, _,
-            [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
+    fun convert _ (PolyML_Pretty.PrettyBreak (width, offset)) = Break (false, width, offset)
+      | convert _ (PolyML_Pretty.PrettyBlock (_, _,
+            [PolyML_Pretty.ContextProperty ("fbrk", _)], [PolyML_Pretty.PrettyString " "])) =
           Break (true, 1, 0)
-      | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) =
+      | convert len (PolyML_Pretty.PrettyBlock (ind, consistent, context, prts)) =
           let
             fun property name default =
-              (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
-                SOME (PolyML.ContextProperty (_, b)) => b
+              (case List.find (fn PolyML_Pretty.ContextProperty (a, _) => name = a | _ => false) context of
+                SOME (PolyML_Pretty.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.PrettyString s) =
+      | convert len (PolyML_Pretty.PrettyString s) =
           String (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
   in convert "" end;