diff -r 5408e5207131 -r d6e492cea6e4 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Feb 06 14:50:55 2010 +0100
@@ -8,7 +8,7 @@
 sig
   val interruptible: ('a -> 'b) -> 'a -> 'b
   val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
-  val system_out: string -> string * int
+  val bash_output: string -> string * int
   structure TimeLimit: TIME_LIMIT
 end;
 
@@ -156,9 +156,9 @@
 end;
 
 
-(* system shell processes, with propagation of interrupts *)
+(* GNU bash processes, with propagation of interrupts *)
 
-fun system_out script = with_attributes no_interrupts (fn orig_atts =>
+fun bash_output script = with_attributes no_interrupts (fn orig_atts =>
   let
     val script_name = OS.FileSys.tmpName ();
     val _ = write_file script_name script;