--- a/src/Pure/ROOT.ML Fri Mar 18 16:38:04 2016 +0100
+++ b/src/Pure/ROOT.ML Fri Mar 18 16:38:40 2016 +0100
@@ -393,8 +393,7 @@
structure Output: OUTPUT = Output; (*seal system channels!*)
-
-use "ML/install_pp_polyml.ML";
+use "ML/ml_pp.ML";
(* the Pure theory *)