src/Pure/System/options.scala

--- a/src/Pure/System/options.scala	Wed Apr 16 09:38:40 2014 +0200
+++ b/src/Pure/System/options.scala	Wed Apr 16 11:52:26 2014 +0200
@@ -52,13 +52,13 @@
 
     def title(strip: String = ""): String =
     {
-      val words = space_explode('_', name)
+      val words = Word.explode('_', name)
       val words1 =
         words match {
           case word :: rest if word == strip => rest
           case _ => words
         }
-      words1.map(Word.capitalize(_)).mkString(" ")
+      Word.implode(words1.map(Word.capitalize(_)))
     }
 
     def unknown: Boolean = typ == Unknown