1.1 --- a/src/Pure/General/scan.scala	Fri Dec 16 12:03:33 2011 +0100
     1.2 +++ b/src/Pure/General/scan.scala	Fri Dec 16 13:37:08 2011 +0100
     1.3 @@ -79,7 +79,7 @@
     1.4  
     1.5      /* pseudo Set methods */
     1.6  
     1.7 -    def iterator: Iterator[String] = content(main_tree, Nil).sortWith(_ <= _).iterator
     1.8 +    def iterator: Iterator[String] = content(main_tree, Nil).sorted.iterator
     1.9  
    1.10      override def toString: String = iterator.mkString("Lexicon(", ", ", ")")
    1.11  

     2.1 --- a/src/Pure/PIDE/document.scala	Fri Dec 16 12:03:33 2011 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Fri Dec 16 13:37:08 2011 +0100
     2.3 @@ -183,8 +183,7 @@
     2.4              for (imp <- header.imports; name <- names.get(imp)) yield(name)
     2.5            case Exn.Exn(_) => Nil
     2.6          }
     2.7 -      Library.topological_order(next,
     2.8 -        Library.sort_wrt((name: Node.Name) => name.node, nodes.keys.toList))
     2.9 +      Library.topological_order(next, nodes.keys.toList.sortBy(_.node))
    2.10      }
    2.11    }
    2.12  

     3.1 --- a/src/Pure/System/isabelle_system.scala	Fri Dec 16 12:03:33 2011 +0100
     3.2 +++ b/src/Pure/System/isabelle_system.scala	Fri Dec 16 13:37:08 2011 +0100
     3.3 @@ -297,7 +297,7 @@
     3.4          for (file <- files if file.isFile) logics += file.getName
     3.5        }
     3.6      }
     3.7 -    logics.toList.sortWith(_ < _)
     3.8 +    logics.toList.sorted
     3.9    }
    3.10  
    3.11  

     4.1 --- a/src/Pure/Thy/completion.scala	Fri Dec 16 12:03:33 2011 +0100
     4.2 +++ b/src/Pure/Thy/completion.scala	Fri Dec 16 13:37:08 2011 +0100
     4.3 @@ -96,7 +96,7 @@
     4.4            case Some(word) =>
     4.5              words_lex.completions(word).map(words_map(_)) match {
     4.6                case Nil => None
     4.7 -              case cs => Some(word, cs.sortWith(_ < _))
     4.8 +              case cs => Some(word, cs.sorted)
     4.9              }
    4.10            case None => None
    4.11          }

     5.1 --- a/src/Pure/library.scala	Fri Dec 16 12:03:33 2011 +0100
     5.2 +++ b/src/Pure/library.scala	Fri Dec 16 13:37:08 2011 +0100
     5.3 @@ -64,18 +64,6 @@
     5.4  
     5.5    def split_lines(str: String): List[String] = space_explode('\n', str)
     5.6  
     5.7 -  def sort_wrt[A](key: A => String, args: Seq[A]): List[A] =
     5.8 -  {
     5.9 -    val ordering: Ordering[A] =
    5.10 -      new Ordering[A] { def compare(x: A, y: A): Int = key(x) compare key(y) }
    5.11 -    val a = (new Array[Any](args.length)).asInstanceOf[Array[A]]
    5.12 -    for ((x, i) <- args.iterator zipWithIndex) a(i) = x
    5.13 -    Sorting.quickSort[A](a)(ordering)
    5.14 -    a.toList
    5.15 -  }
    5.16 -
    5.17 -  def sort_strings(args: Seq[String]): List[String] = sort_wrt((x: String) => x, args)
    5.18 -
    5.19  
    5.20    /* iterate over chunks (cf. space_explode) */
    5.21  

     6.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Dec 16 12:03:33 2011 +0100
     6.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Dec 16 13:37:08 2011 +0100
     6.3 @@ -96,7 +96,7 @@
     6.4              case Some((word, cs)) =>
     6.5                val ds =
     6.6                  (if (Isabelle_Encoding.is_active(buffer))
     6.7 -                  cs.map(Symbol.decode(_)).sortWith(_ < _)
     6.8 +                  cs.map(Symbol.decode(_)).sorted
     6.9                   else cs).filter(_ != word)
    6.10                if (ds.isEmpty) null
    6.11                else new SideKickCompletion(

     7.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Dec 16 12:03:33 2011 +0100
     7.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Dec 16 13:37:08 2011 +0100
     7.3 @@ -379,7 +379,7 @@
     7.4          filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))
     7.5  
     7.6        if (!files.isEmpty) {
     7.7 -        val files_list = new ListView(Library.sort_strings(files))
     7.8 +        val files_list = new ListView(files.sorted)
     7.9          for (i <- 0 until files.length)
    7.10            files_list.selection.indices += i
    7.11