--- 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 *)