src/Pure/POLY.ML

         in close_in is;
            close_out os;
            implode result
         end;
 
-fun delete_file name = ExtendedIO.execute ("rm " ^ name);
+(*Delete a file *)
+fun delete_file name =
+  let val (_,_) = ExtendedIO.execute ("rm " ^ name)
+  in () end;