diff -r 97800f7e80b4 -r b58d6a33b57f src/Pure/ML-Systems/install_pp_polyml.ML
--- a/src/Pure/ML-Systems/install_pp_polyml.ML	Sun May 31 15:03:34 2009 +0200
+++ b/src/Pure/ML-Systems/install_pp_polyml.ML	Sun May 31 15:07:03 2009 +0200
@@ -3,15 +3,17 @@
 Extra toplevel pretty-printing for Poly/ML.
 *)
 
-install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
-  (case Future.peek x of
-    NONE => str "<future>"
-  | SOME (Exn.Exn _) => str "<failed>"
-  | SOME (Exn.Result y) => print (y, depth)));
+PolyML.install_pp
+  (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
+    (case Future.peek x of
+      NONE => str "<future>"
+    | SOME (Exn.Exn _) => str "<failed>"
+    | SOME (Exn.Result y) => print (y, depth)));
 
-install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
-  (case Lazy.peek x of
-    NONE => str "<lazy>"
-  | SOME (Exn.Exn _) => str "<failed>"
-  | SOME (Exn.Result y) => print (y, depth)));
+PolyML.install_pp
+  (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
+    (case Lazy.peek x of
+      NONE => str "<lazy>"
+    | SOME (Exn.Exn _) => str "<failed>"
+    | SOME (Exn.Result y) => print (y, depth)));