diff -r b1a87e3971a3 -r 88bc86d7dec3 src/Pure/ML-Systems/install_pp_polyml-experimental.ML
--- a/src/Pure/ML-Systems/install_pp_polyml-experimental.ML	Tue Mar 24 22:56:17 2009 +0100
+++ b/src/Pure/ML-Systems/install_pp_polyml-experimental.ML	Tue Mar 24 23:43:58 2009 +0100
@@ -4,24 +4,15 @@
 Poly/ML 5.3.
 *)
 
-local
-
-fun pretty_future depth (pretty: 'a * int -> pretty) (x: 'a future) =
+addPrettyPrinter (fn depth => fn pretty => fn x =>
   (case Future.peek x of
     NONE => PrettyString "<future>"
   | SOME (Exn.Exn _) => PrettyString "<failed>"
-  | SOME (Exn.Result y) => pretty (y, depth));
+  | SOME (Exn.Result y) => pretty (y, depth)));
 
-fun pretty_lazy depth (pretty: 'a * int -> pretty) (x: 'a lazy) =
+addPrettyPrinter (fn depth => fn pretty => fn x =>
   (case Lazy.peek x of
     NONE => PrettyString "<lazy>"
   | SOME (Exn.Exn _) => PrettyString "<failed>"
-  | SOME (Exn.Result y) => pretty (y, depth));
-
-in
+  | SOME (Exn.Result y) => pretty (y, depth)));
 
-val _ = addPrettyPrinter pretty_future;
-val _ = addPrettyPrinter pretty_lazy;
-
-end;
-