# HG changeset patch
# User wenzelm
# Date 1243775223 -7200
# Node ID b58d6a33b57fee8fba4a531a503afa5b7a75d13b
# Parent  97800f7e80b46cc54f4ba2e7980a3cbc2e5b5c22
explicit PolyML.install_pp;

diff -r 97800f7e80b4 -r b58d6a33b57f src/Pure/ML-Systems/install_pp_polyml.ML
--- 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)));