# HG changeset patch
# User wenzelm
# Date 1459624207 -7200
# Node ID d3ff367a16a0168da59de43bcc2957789fa8a640
# Parent  2733b240bfeab3dd078ded9a617101d2ef55febb
careful export of type-dependent functions, without losing their special status;

diff -r 2733b240bfea -r d3ff367a16a0 Admin/polyml/future/ROOT.ML
--- a/Admin/polyml/future/ROOT.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/Admin/polyml/future/ROOT.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -116,16 +116,16 @@
 use "Concurrent/mailbox.ML";
 use "Concurrent/cache.ML";
 
-PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
+ML_system_pp (fn depth => fn pretty => fn var =>
   pretty (Synchronized.value var, depth));
 
-PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
+ML_system_pp (fn depth => fn pretty => fn x =>
   (case Future.peek x of
     NONE => PolyML.PrettyString "<future>"
   | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
   | SOME (Exn.Res y) => pretty (y, depth)));
 
-PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
+ML_system_pp (fn depth => fn pretty => fn x =>
   (case Lazy.peek x of
     NONE => PolyML.PrettyString "<lazy>"
   | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Concurrent/future.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -100,7 +100,7 @@
 fun is_finished x = is_some (peek x);
 
 val _ =
-  PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
+  ML_system_pp (fn depth => fn pretty => fn x =>
     (case peek x of
       NONE => PolyML.PrettyString "<future>"
     | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -103,7 +103,7 @@
 (* toplevel pretty printing *)
 
 val _ =
-  PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
+  ML_system_pp (fn depth => fn pretty => fn x =>
     (case peek x of
       NONE => PolyML.PrettyString "<lazy>"
     | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -69,6 +69,6 @@
 
 (* toplevel pretty printing *)
 
-val _ = PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => pretty (value var, depth));
+val _ = ML_system_pp (fn depth => fn pretty => fn var => pretty (value var, depth));
 
 end;
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -397,7 +397,7 @@
 
 (* toplevel pretty printing *)
 
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_task);
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_group);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_task);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_group);
 
 end;
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/General/binding.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -154,7 +154,7 @@
 
 val print = Pretty.unformatted_string_of o pretty;
 
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty o set_pos Position.none);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty o set_pos Position.none);
 
 
 (* check *)
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/General/linear_set.ML
--- a/src/Pure/General/linear_set.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/General/linear_set.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -136,11 +136,11 @@
 (* ML pretty-printing *)
 
 val _ =
-  PolyML.addPrettyPrinter (fn depth => fn pretty => fn set =>
+  ML_system_pp (fn depth => fn pretty => fn set =>
     ML_Pretty.to_polyml
       (ML_Pretty.enum "," "{" "}"
         (ML_Pretty.pair
-          (ML_Pretty.from_polyml o PolyML.prettyRepresentation)
+          (ML_Pretty.from_polyml o ML_system_pretty)
           (ML_Pretty.from_polyml o pretty))
         (dest set, depth)));
 
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/General/path.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -173,7 +173,7 @@
 
 val print = Pretty.unformatted_string_of o pretty;
 
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);
 
 
 (* base element *)
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/General/pretty.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -402,7 +402,7 @@
 
 end;
 
-val _ = PolyML.addPrettyPrinter (fn d => fn _ => ML_Pretty.to_polyml o to_ML (d + 1) o quote);
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => to_polyml o position);
+val _ = ML_system_pp (fn d => fn _ => ML_Pretty.to_polyml o to_ML (d + 1) o quote);
+val _ = ML_system_pp (fn _ => fn _ => to_polyml o position);
 
 end;
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/General/sha1.ML
--- a/src/Pure/General/sha1.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/General/sha1.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -182,7 +182,7 @@
 fun rep (Digest s) = s;
 val fake = Digest;
 
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o rep);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o rep);
 
 fun digest_string str = digest_string_external str
   handle CInterface.Foreign msg =>
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/General/table.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -411,11 +411,11 @@
 (* ML pretty-printing *)
 
 val _ =
-  PolyML.addPrettyPrinter (fn depth => fn pretty => fn tab =>
+  ML_system_pp (fn depth => fn pretty => fn tab =>
     ML_Pretty.to_polyml
       (ML_Pretty.enum "," "{" "}"
         (ML_Pretty.pair
-          (ML_Pretty.from_polyml o PolyML.prettyRepresentation)
+          (ML_Pretty.from_polyml o ML_system_pretty)
           (ML_Pretty.from_polyml o pretty))
         (dest tab, depth)));
 
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -174,7 +174,7 @@
       (context * thm list list -> context -> context)};
 
 val _ =
-  PolyML.addPrettyPrinter (fn _ => fn _ => fn _: state =>
+  ML_system_pp (fn _ => fn _ => fn _: state =>
     Pretty.to_polyml (Pretty.str "<Proof.state>"));
 
 fun make_goal (statement, using, goal, before_qed, after_qed) =
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Isar/runtime.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -43,7 +43,7 @@
 fun pretty_exn (exn: exn) =
   Pretty.from_ML
     (ML_Pretty.from_polyml
-      (PolyML.prettyRepresentation (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
+      (ML_system_pretty (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
 
 
 (* exn_context *)
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -199,7 +199,7 @@
 
 fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
 
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_abstract);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_abstract);
 
 
 
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/ML/ml_compiler0.ML
--- a/src/Pure/ML/ml_compiler0.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/ML/ml_compiler0.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -139,3 +139,15 @@
         {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
       handle ERROR msg => (#print context msg; raise error "ML error"))
   end;
+
+
+(* export type-dependent functions *)
+
+ML_Compiler0.use_text
+  (ML_Compiler0.make_context
+    (ML_Name_Space.global_values
+      [("prettyRepresentation", "ML_system_pretty"),
+       ("addPrettyPrinter", "ML_system_pp"),
+       ("addOverload", "ML_system_overload")]))
+  {debug = false, file = "", line = 0, verbose = false}
+  "open PolyML RunCall";
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/ML/ml_debugger.ML
--- a/src/Pure/ML/ml_debugger.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/ML/ml_debugger.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -42,7 +42,7 @@
 end;
 
 val _ =
-  PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
+  ML_system_pp (fn _ => fn _ => fn exn_id =>
     let val s = print_exn_id exn_id
     in ML_Pretty.to_polyml (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
 
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/ML/ml_name_space.ML
--- a/src/Pure/ML/ml_name_space.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -11,7 +11,31 @@
   open PolyML.NameSpace;
 
   type T = PolyML.NameSpace.nameSpace;
+
   val global = PolyML.globalNameSpace;
+  fun global_values values : T =
+   {lookupVal = #lookupVal global,
+    lookupType = #lookupType global,
+    lookupStruct = #lookupStruct global,
+    lookupFix = #lookupFix global,
+    lookupSig = #lookupSig global,
+    lookupFunct = #lookupFunct global,
+    enterVal =
+      fn (x, value) =>
+        (case List.find (fn (y, _) => x = y) values of
+          SOME (_, x') => #enterVal global (x', value)
+        | NONE => ()),
+    enterType = fn _ => (),
+    enterFix = fn _ => (),
+    enterStruct = fn _ => (),
+    enterSig = fn _ => (),
+    enterFunct = fn _ => (),
+    allVal = #allVal global,
+    allType = #allType global,
+    allFix = #allFix global,
+    allStruct = #allStruct global,
+    allSig = #allSig global,
+    allFunct = #allFunct global};
 
   type valueVal = Values.value;
   fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/ML/ml_pp.ML
--- a/src/Pure/ML/ml_pp.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/ML/ml_pp.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -8,22 +8,22 @@
 struct
 
 val _ =
-  PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
+  ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
 
 val _ =
-  PolyML.addPrettyPrinter (fn depth => fn _ =>
+  ML_system_pp (fn depth => fn _ =>
     ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Thy_Info.pure_theory);
 
 val _ =
-  PolyML.addPrettyPrinter (fn depth => fn _ =>
+  ML_system_pp (fn depth => fn _ =>
     ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Thy_Info.pure_theory);
 
 val _ =
-  PolyML.addPrettyPrinter (fn depth => fn _ =>
+  ML_system_pp (fn depth => fn _ =>
     ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Thy_Info.pure_theory);
 
 val _ =
-  PolyML.addPrettyPrinter (fn depth => fn _ =>
+  ML_system_pp (fn depth => fn _ =>
     ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Thy_Info.pure_theory);
 
 
@@ -43,17 +43,17 @@
         |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
     | Abs (a, T, b) =>
         prt_apps "Abs"
-         [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
-          Pretty.from_polyml (PolyML.prettyRepresentation (T, dp - 2)),
+         [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
+          Pretty.from_polyml (ML_system_pretty (T, dp - 2)),
           prt_term false (dp - 3) b]
-    | Const a => prt_app "Const" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
-    | Free a => prt_app "Free" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
-    | Var a => prt_app "Var" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
-    | Bound a => prt_app "Bound" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1))));
+    | Const a => prt_app "Const" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
+    | Free a => prt_app "Free" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
+    | Var a => prt_app "Var" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
+    | Bound a => prt_app "Bound" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))));
 
 in
 
-val _ = PolyML.addPrettyPrinter (fn depth => fn _ => Pretty.to_polyml o prt_term false depth);
+val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o prt_term false depth);
 
 
 local
@@ -66,22 +66,22 @@
     | _ %% _ => prt_proofs parens dp prf
     | Abst (a, T, b) =>
         prt_apps "Abst"
-         [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
-          Pretty.from_polyml (PolyML.prettyRepresentation (T, dp - 2)),
+         [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
+          Pretty.from_polyml (ML_system_pretty (T, dp - 2)),
           prt_proof false (dp - 3) b]
     | AbsP (a, t, b) =>
         prt_apps "AbsP"
-         [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
-          Pretty.from_polyml (PolyML.prettyRepresentation (t, dp - 2)),
+         [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
+          Pretty.from_polyml (ML_system_pretty (t, dp - 2)),
           prt_proof false (dp - 3) b]
     | Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t)
     | MinProof => Pretty.str "MinProof"
-    | PBound a => prt_app "PBound" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
-    | PAxm a => prt_app "PAxm" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
-    | OfClass a => prt_app "OfClass" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
-    | Oracle a => prt_app "Oracle" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
-    | Promise a => prt_app "Promise" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
-    | PThm a => prt_app "PThm" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1))))
+    | PBound a => prt_app "PBound" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
+    | PAxm a => prt_app "PAxm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
+    | OfClass a => prt_app "OfClass" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
+    | Oracle a => prt_app "Oracle" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
+    | Promise a => prt_app "Promise" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
+    | PThm a => prt_app "PThm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))))
 
 and prt_proofs parens dp prf =
   let
@@ -94,7 +94,7 @@
       strip_proof p
         ((fn d =>
           [Pretty.str " %", Pretty.brk 1,
-            Pretty.from_polyml (PolyML.prettyRepresentation (t, d))]) :: res)
+            Pretty.from_polyml (ML_system_pretty (t, d))]) :: res)
   | strip_proof (p %% q) res =
       strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d q]) :: res)
   | strip_proof p res = (fn d => prt_proof true d p, res);
@@ -102,7 +102,7 @@
 in
 
 val _ =
-  PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
+  ML_system_pp (fn depth => fn _ => fn prf =>
     ML_Pretty.to_polyml (Pretty.to_ML ~1 (prt_proof false depth prf)));
 
 end;
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/ML/ml_pretty.ML
--- a/src/Pure/ML/ml_pretty.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -116,7 +116,7 @@
 
 local
   fun pretty_string_of s = "(fn x => Pretty.string_of (Pretty.from_polyml (" ^ s ^ ")))";
-  fun pretty_value depth = "PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^ depth ^ "))";
+  fun pretty_value depth = "ML_system_pretty (x, FixedInt.fromInt (" ^ depth ^ "))";
 in
 
 fun make_string_fn local_env =
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -124,7 +124,7 @@
   in Pretty.str (quote (implode (map print_char body'))) end;
 
 val _ =
-  PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
+  ML_system_pp (fn depth => fn _ => fn str =>
     Pretty.to_polyml (pretty_string (FixedInt.toInt (depth * 100)) str));
 
 end;
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/PIDE/xml.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -170,8 +170,7 @@
 fun pretty depth tree =
   Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
 
-val _ =
-  PolyML.addPrettyPrinter (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
+val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
 
 
 
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Syntax/ast.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -66,7 +66,7 @@
 fun pretty_rule (lhs, rhs) =
   Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];
 
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_ast);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_ast);
 
 
 (* strip_positions *)
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -451,7 +451,7 @@
 (* toplevel pretty printing *)
 
 val _ =
-  PolyML.addPrettyPrinter (fn _ => fn _ =>
+  ML_system_pp (fn _ => fn _ =>
     Pretty.to_polyml o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon);
 
 end;
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/context.ML
--- a/src/Pure/context.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/context.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -169,7 +169,7 @@
 
 val pretty_thy = Pretty.str_list "{" "}" o display_names;
 
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_thy);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_thy);
 
 fun pretty_abbrev_thy thy =
   let
diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/morphism.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -71,7 +71,7 @@
 
 fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names));
 
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);
 
 fun binding (Morphism {binding, ...}) = apply binding;
 fun typ (Morphism {typ, ...}) = apply typ;