# HG changeset patch
# User wenzelm
# Date 1223899014 -7200
# Node ID 81d97311c0578802634022a2eaef66a76d9150fc
# Parent  8789a0abccaa68144eace059ec6d625eefff6c40
tuned output;

diff -r 8789a0abccaa -r 81d97311c057 src/Pure/ML-Systems/install_pp_polyml.ML
--- a/src/Pure/ML-Systems/install_pp_polyml.ML	Mon Oct 13 13:44:59 2008 +0200
+++ b/src/Pure/ML-Systems/install_pp_polyml.ML	Mon Oct 13 13:56:54 2008 +0200
@@ -7,7 +7,7 @@
 install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Future.T) =>
   (case Future.peek x of
     NONE => str "<future>"
-  | SOME (Exn.Exn _) => str "<failed 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 Susp.T) =>