--- 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)));