# HG changeset patch
# User wenzelm
# Date 1313604516 -7200
# Node ID 380a4677c55dd61c6a24a9a18cf0117d6b2784ef
# Parent  45fb4b29c2679bb82e4a178043ff3424a9adaf77
tuned signature;

diff -r 45fb4b29c267 -r 380a4677c55d src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Wed Aug 17 18:52:21 2011 +0200
+++ b/src/Pure/General/exn.ML	Wed Aug 17 20:08:36 2011 +0200
@@ -11,7 +11,6 @@
   val get_exn: 'a result -> exn option
   val capture: ('a -> 'b) -> 'a -> 'b result
   val release: 'a result -> 'a
-  val flat_result: 'a result result -> 'a result
   val map_result: ('a -> 'b) -> 'a result -> 'b result
   val maps_result: ('a -> 'b result) -> 'a result -> 'b result
   exception Interrupt
@@ -47,13 +46,10 @@
 fun release (Res y) = y
   | release (Exn e) = reraise e;
 
-fun flat_result (Res x) = x
-  | flat_result (Exn e) = Exn e;
-
 fun map_result f (Res x) = Res (f x)
   | map_result f (Exn e) = Exn e;
 
-fun maps_result f = flat_result o map_result f;
+fun maps_result f = (fn Res x => x | Exn e => Exn e) o map_result f;
 
 
 (* interrupts *)