# HG changeset patch
# User wenzelm
# Date 1237934638 -3600
# Node ID 88bc86d7dec3814562530f5b176cad0067806a02
# Parent  b1a87e3971a3a09b47078e2ea27999a4d3255a60
simplified addPrettyPrinter setup: may pass (fn ...) directly if type constraints are omitted -- addPrettyPrinter treated as a special case internally;

diff -r b1a87e3971a3 -r 88bc86d7dec3 src/Pure/ML-Systems/install_pp_polyml-experimental.ML
--- a/src/Pure/ML-Systems/install_pp_polyml-experimental.ML	Tue Mar 24 22:56:17 2009 +0100
+++ b/src/Pure/ML-Systems/install_pp_polyml-experimental.ML	Tue Mar 24 23:43:58 2009 +0100
@@ -4,24 +4,15 @@
 Poly/ML 5.3.
 *)
 
-local
-
-fun pretty_future depth (pretty: 'a * int -> pretty) (x: 'a future) =
+addPrettyPrinter (fn depth => fn pretty => fn x =>
   (case Future.peek x of
     NONE => PrettyString "<future>"
   | SOME (Exn.Exn _) => PrettyString "<failed>"
-  | SOME (Exn.Result y) => pretty (y, depth));
+  | SOME (Exn.Result y) => pretty (y, depth)));
 
-fun pretty_lazy depth (pretty: 'a * int -> pretty) (x: 'a lazy) =
+addPrettyPrinter (fn depth => fn pretty => fn x =>
   (case Lazy.peek x of
     NONE => PrettyString "<lazy>"
   | SOME (Exn.Exn _) => PrettyString "<failed>"
-  | SOME (Exn.Result y) => pretty (y, depth));
-
-in
+  | SOME (Exn.Result y) => pretty (y, depth)));
 
-val _ = addPrettyPrinter pretty_future;
-val _ = addPrettyPrinter pretty_lazy;
-
-end;
-