src/Pure/ML/install_pp_polyml.ML
changeset 43761 e72ba84ae58f
parent 38327 d6afb77b0f6d
child 47986 ca7104aebb74
--- a/src/Pure/ML/install_pp_polyml.ML	Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/ML/install_pp_polyml.ML	Mon Jul 11 22:55:47 2011 +0200
@@ -9,12 +9,12 @@
     (case Future.peek x of
       NONE => str "<future>"
     | SOME (Exn.Exn _) => str "<failed>"
-    | SOME (Exn.Result y) => print (y, depth)));
+    | SOME (Exn.Res 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)));
+    | SOME (Exn.Res y) => print (y, depth)));