tuned output;
authorwenzelm
Mon, 13 Oct 2008 13:56:54 +0200
changeset 28570 81d97311c057
parent 28569 8789a0abccaa
child 28571 47d88239658d
tuned output;
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) =>