diff --git a/src/Pure/General/exn.ML b/src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML
+++ b/src/Pure/General/exn.ML
@@ -1,132 +1,129 @@
 (*  Title:      Pure/General/exn.ML
     Author:     Makarius
 
 Support for exceptions.
 *)
 
 signature BASIC_EXN =
 sig
   exception ERROR of string
   val error: string -> 'a
   val cat_error: string -> string -> 'a
 end;
 
 signature EXN =
 sig
   include BASIC_EXN
   val polyml_location: exn -> PolyML.location option
   val reraise: exn -> 'a
   datatype 'a result = Res of 'a | Exn of exn
   val get_res: 'a result -> 'a option
   val get_exn: 'a result -> exn option
   val capture: ('a -> 'b) -> 'a -> 'b result
   val release: 'a result -> 'a
   val map_res: ('a -> 'b) -> 'a result -> 'b result
   val maps_res: ('a -> 'b result) -> 'a result -> 'b result
   val map_exn: (exn -> exn) -> 'a result -> 'a result
   exception Interrupt
   val interrupt: unit -> 'a
   val is_interrupt: exn -> bool
   val interrupt_exn: 'a result
   val is_interrupt_exn: 'a result -> bool
   val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
-  val interrupt_return_code: int
   val return_code: exn -> int -> int
   val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
   exception EXCEPTIONS of exn list
   val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
 end;
 
 structure Exn: EXN =
 struct
 
 (* location *)
 
 val polyml_location = PolyML.Exception.exceptionLocation;
 
 val reraise = PolyML.Exception.reraise;
 
 
 (* user errors *)
 
 exception ERROR of string;
 
 fun error msg = raise ERROR msg;
 
 fun cat_error "" msg = error msg
   | cat_error msg "" = error msg
   | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
 
 
 (* exceptions as values *)
 
 datatype 'a result =
   Res of 'a |
   Exn of exn;
 
 fun get_res (Res x) = SOME x
   | get_res _ = NONE;
 
 fun get_exn (Exn exn) = SOME exn
   | get_exn _ = NONE;
 
 fun capture f x = Res (f x) handle e => Exn e;
 
 fun release (Res y) = y
   | release (Exn e) = reraise e;
 
 fun map_res f (Res x) = Res (f x)
   | map_res f (Exn e) = Exn e;
 
 fun maps_res f = (fn Res x => x | Exn e => Exn e) o map_res f;
 
 fun map_exn f (Res x) = Res x
   | map_exn f (Exn e) = Exn (f e);
 
 
 (* interrupts *)
 
 exception Interrupt = Thread.Thread.Interrupt;
 
 fun interrupt () = raise Interrupt;
 
 fun is_interrupt Interrupt = true
   | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause
   | is_interrupt _ = false;
 
 val interrupt_exn = Exn Interrupt;
 
 fun is_interrupt_exn (Exn exn) = is_interrupt exn
   | is_interrupt_exn _ = false;
 
 fun interruptible_capture f x =
   Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
 
 
 (* POSIX return code *)
 
-val interrupt_return_code : int = 130;
-
 fun return_code exn rc =
-  if is_interrupt exn then interrupt_return_code else rc;
+  if is_interrupt exn then 130 else rc;
 
 fun capture_exit rc f x =
   f x handle exn => exit (return_code exn rc);
 
 
 (* concatenated exceptions *)
 
 exception EXCEPTIONS of exn list;
 
 
 (* low-level trace *)
 
 fun trace exn_message output e =
   PolyML.Exception.traceException
     (e, fn (trace, exn) =>
       let
         val title = "Exception trace - " ^ exn_message exn;
         val () = output (String.concatWith "\n" (title :: trace));
       in reraise exn end);
 
 end;
diff --git a/src/Pure/System/process_result.ML b/src/Pure/System/process_result.ML
--- a/src/Pure/System/process_result.ML
+++ b/src/Pure/System/process_result.ML
@@ -1,61 +1,53 @@
 (*  Title:      Pure/System/process_result.scala
     Author:     Makarius
 
 Result of system process.
 *)
 
 signature PROCESS_RESULT =
 sig
   type T
   val make:
    {rc: int,
     out_lines: string list,
     err_lines: string list,
     timing: Timing.timing} -> T
   val rc: T -> int
   val out_lines: T -> string list
   val err_lines: T -> string list
   val timing: T -> Timing.timing
   val out: T -> string
   val err: T -> string
   val ok: T -> bool
-  val interrupted: T -> bool
-  val check_rc: (int -> bool) -> T -> T
   val check: T -> T
 end;
 
 structure Process_Result: PROCESS_RESULT =
 struct
 
 abstype T =
   Process_Result of
    {rc: int,
     out_lines: string list,
     err_lines: string list,
     timing: Timing.timing}
 with
 
 val make = Process_Result;
 fun rep (Process_Result args) = args;
 
 val rc = #rc o rep;
 val out_lines = #out_lines o rep;
 val err_lines = #err_lines o rep;
 val timing = #timing o rep;
 
 val out = trim_line o cat_lines o out_lines;
 val err = trim_line o cat_lines o err_lines;
 
 fun ok result = rc result = 0;
-fun interrupted result = rc result = Exn.interrupt_return_code;
 
-fun check_rc pred result =
-  if pred (rc result) then result
-  else if interrupted result then raise Exn.Interrupt
-  else error (err result);
-
-val check = check_rc (fn rc => rc = 0);
+fun check result = if ok result then result else error (err result);
 
 end;
 
 end;