src/Pure/ML-Systems/install_pp_polyml.ML
changeset 28975 ec120dc11e8b
parent 28673 d746a8c12c43
child 29564 f8b933a62151
--- 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>"