1.1 --- a/src/Pure/library.scala	Fri Dec 16 12:03:33 2011 +0100
     1.2 +++ b/src/Pure/library.scala	Fri Dec 16 13:37:08 2011 +0100
     1.3 @@ -64,18 +64,6 @@
     1.4  
     1.5    def split_lines(str: String): List[String] = space_explode('\n', str)
     1.6  
     1.7 -  def sort_wrt[A](key: A => String, args: Seq[A]): List[A] =
     1.8 -  {
     1.9 -    val ordering: Ordering[A] =
    1.10 -      new Ordering[A] { def compare(x: A, y: A): Int = key(x) compare key(y) }
    1.11 -    val a = (new Array[Any](args.length)).asInstanceOf[Array[A]]
    1.12 -    for ((x, i) <- args.iterator zipWithIndex) a(i) = x
    1.13 -    Sorting.quickSort[A](a)(ordering)
    1.14 -    a.toList
    1.15 -  }
    1.16 -
    1.17 -  def sort_strings(args: Seq[String]): List[String] = sort_wrt((x: String) => x, args)
    1.18 -
    1.19  
    1.20    /* iterate over chunks (cf. space_explode) */
    1.21