diff -r 519b6e53179b -r a45ba78abcc1 src/Pure/System/command_line.ML
--- a/src/Pure/System/command_line.ML	Wed Aug 08 12:13:34 2012 +0200
+++ b/src/Pure/System/command_line.ML	Wed Aug 08 12:33:40 2012 +0200
@@ -6,7 +6,7 @@
 
 signature COMMAND_LINE =
 sig
-  val tool: (unit -> int) -> 'a
+  val tool: (unit -> int) -> unit
 end;
 
 structure Command_Line: COMMAND_LINE =
@@ -17,7 +17,7 @@
     let val rc =
       restore_attributes body () handle exn =>
         (Output.error_msg (ML_Compiler.exn_message exn); if Exn.is_interrupt exn then 130 else 1);
-    in exit rc; raise Fail "ERROR" end) ();
+    in if rc = 0 then () else exit rc end) ();
 
 end;