List.flatten

It seems this method has been deprecated in object List, and removed  
in class List. The deprecation message says one should use the missing  
method on class List:

   /** Concatenate all the elements of a given list of lists.
    *
    *   <at> param xss the list of lists that are to be concatenated
    *   <at> return    the concatenation of all the lists
    */
    <at> deprecated("use `xss.flatten' instead")
   def flatten[A](xss: List[List[A]]): List[A] = {

Is there a problem if I undeprecate it? Grepping the compiler showed  
that it is still used in a couple of places.

iulian

--
Iulian Dragos
--
http://lamp.epfl.ch/~dragos