--- a/src/Pure/ML-Systems/install_pp_polyml.ML Thu Dec 04 23:01:03 2008 +0100
+++ b/src/Pure/ML-Systems/install_pp_polyml.ML Thu Dec 04 23:01:11 2008 +0100
@@ -4,13 +4,13 @@
Extra toplevel pretty-printing for Poly/ML.
*)
-install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Future.T) =>
+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.T) =>
+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>"