src/Pure/General/completion.scala

--- a/src/Pure/General/completion.scala	Sat Mar 15 11:59:18 2014 +0100
+++ b/src/Pure/General/completion.scala	Sat Mar 15 12:51:14 2014 +0100
@@ -86,10 +86,16 @@
     def ordering: Ordering[Item] =
       new Ordering[Item] {
         def compare(item1: Item, item2: Item): Int =
+          frequency(item2.name) compare frequency(item1.name)
+      }
+
+    def name_ordering: Ordering[Item] =
+      new Ordering[Item] {
+        def compare(item1: Item, item2: Item): Int =
         {
-          frequency(item1.name) compare frequency(item2.name) match {
+          frequency(item2.name) compare frequency(item2.name) match {
             case 0 => item1.name compare item2.name
-            case ord => - ord
+            case ord => ord
           }
         }
       }
@@ -415,7 +421,7 @@
           yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)
 
         if (items.isEmpty) None
-        else Some(Completion.Result(range, original, unique, items.sorted(history.ordering)))
+        else Some(Completion.Result(range, original, unique, items.sorted(history.name_ordering)))
 
       case _ => None
     }