1.1 --- a/src/Pure/System/command_line.ML	Thu Feb 28 14:29:54 2013 +0100
     1.2 +++ b/src/Pure/System/command_line.ML	Thu Feb 28 16:19:08 2013 +0100
     1.3 @@ -7,6 +7,7 @@
     1.4  signature COMMAND_LINE =
     1.5  sig
     1.6    val tool: (unit -> int) -> unit
     1.7 +  val tool0: (unit -> unit) -> unit
     1.8  end;
     1.9  
    1.10  structure Command_Line: COMMAND_LINE =
    1.11 @@ -19,5 +20,7 @@
    1.12          (Output.error_msg (ML_Compiler.exn_message exn); if Exn.is_interrupt exn then 130 else 1);
    1.13      in if rc = 0 then () else exit rc end) ();
    1.14  
    1.15 +fun tool0 body = tool (fn () => (body (); 0));
    1.16 +
    1.17  end;
    1.18