1.1 --- a/src/Pure/General/exn.ML	Wed Aug 17 20:08:36 2011 +0200
     1.2 +++ b/src/Pure/General/exn.ML	Wed Aug 17 22:14:22 2011 +0200
     1.3 @@ -20,10 +20,6 @@
     1.4    val is_interrupt_exn: 'a result -> bool
     1.5    val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
     1.6    exception EXCEPTIONS of exn list
     1.7 -  val flatten: exn -> exn list
     1.8 -  val flatten_list: exn list -> exn list
     1.9 -  val release_all: 'a result list -> 'a list
    1.10 -  val release_first: 'a result list -> 'a list
    1.11  end;
    1.12  
    1.13  structure Exn: EXN =
    1.14 @@ -71,23 +67,10 @@
    1.15    Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
    1.16  
    1.17  
    1.18 -(* nested exceptions *)
    1.19 +(* concatenated exceptions *)
    1.20  
    1.21  exception EXCEPTIONS of exn list;
    1.22  
    1.23 -fun flatten (EXCEPTIONS exns) = flatten_list exns
    1.24 -  | flatten exn = if is_interrupt exn then [] else [exn]
    1.25 -and flatten_list exns = List.concat (map flatten exns);
    1.26 -
    1.27 -fun release_all results =
    1.28 -  if List.all (fn Res _ => true | _ => false) results
    1.29 -  then map (fn Res x => x) results
    1.30 -  else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
    1.31 -
    1.32 -fun release_first results = release_all results
    1.33 -  handle EXCEPTIONS [] => interrupt ()
    1.34 -    | EXCEPTIONS (exn :: _) => reraise exn;
    1.35 -
    1.36  end;
    1.37  
    1.38  datatype illegal = Interrupt;