# HG changeset patch
# User haftmann
# Date 1284648693 -7200
# Node ID 1cf49add5b400b811eb3a50575aed24154b58b9f
# Parent  55e0ff582fa4c47c28016b5077903ebd59e85e0e
Exn.map_result

diff -r 55e0ff582fa4 -r 1cf49add5b40 src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Thu Sep 16 16:51:33 2010 +0200
+++ b/src/Pure/General/exn.ML	Thu Sep 16 16:51:33 2010 +0200
@@ -11,6 +11,7 @@
   val get_exn: 'a result -> exn option
   val capture: ('a -> 'b) -> 'a -> 'b result
   val release: 'a result -> 'a
+  val map_result: ('a -> 'a) -> 'a result -> 'a result
   exception Interrupt
   val interrupt: unit -> 'a
   val is_interrupt: exn -> bool
@@ -43,6 +44,9 @@
 fun release (Result y) = y
   | release (Exn e) = reraise e;
 
+fun map_result f (Result x) = Result (f x)
+  | map_result f e = e;
+
 
 (* interrupts *)