1.1 --- a/src/Pure/General/exn.ML	Wed Aug 17 18:52:21 2011 +0200
     1.2 +++ b/src/Pure/General/exn.ML	Wed Aug 17 20:08:36 2011 +0200
     1.3 @@ -11,7 +11,6 @@
     1.4    val get_exn: 'a result -> exn option
     1.5    val capture: ('a -> 'b) -> 'a -> 'b result
     1.6    val release: 'a result -> 'a
     1.7 -  val flat_result: 'a result result -> 'a result
     1.8    val map_result: ('a -> 'b) -> 'a result -> 'b result
     1.9    val maps_result: ('a -> 'b result) -> 'a result -> 'b result
    1.10    exception Interrupt
    1.11 @@ -47,13 +46,10 @@
    1.12  fun release (Res y) = y
    1.13    | release (Exn e) = reraise e;
    1.14  
    1.15 -fun flat_result (Res x) = x
    1.16 -  | flat_result (Exn e) = Exn e;
    1.17 -
    1.18  fun map_result f (Res x) = Res (f x)
    1.19    | map_result f (Exn e) = Exn e;
    1.20  
    1.21 -fun maps_result f = flat_result o map_result f;
    1.22 +fun maps_result f = (fn Res x => x | Exn e => Exn e) o map_result f;
    1.23  
    1.24  
    1.25  (* interrupts *)