src/Pure/System/command_line.ML

--- a/src/Pure/System/command_line.ML	Thu Feb 28 14:29:54 2013 +0100
+++ b/src/Pure/System/command_line.ML	Thu Feb 28 16:19:08 2013 +0100
@@ -7,6 +7,7 @@
 signature COMMAND_LINE =
 sig
   val tool: (unit -> int) -> unit
+  val tool0: (unit -> unit) -> unit
 end;
 
 structure Command_Line: COMMAND_LINE =
@@ -19,5 +20,7 @@
         (Output.error_msg (ML_Compiler.exn_message exn); if Exn.is_interrupt exn then 130 else 1);
     in if rc = 0 then () else exit rc end) ();
 
+fun tool0 body = tool (fn () => (body (); 0));
+
 end;