# HG changeset patch
# User wenzelm
# Date 1228428071 -3600
# Node ID ec120dc11e8b0096a1e2323f2b1b91b01377b74e
# Parent  d6b190efa01a352cffc272ba5cc25d6754257041
renamed type Lazy.T to lazy;
renamed type Future.T to future;

diff -r d6b190efa01a -r ec120dc11e8b src/Pure/ML-Systems/install_pp_polyml.ML
--- 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>"