src/Pure/library.scala

--- a/src/Pure/library.scala	Fri Mar 07 13:29:10 2014 +0100
+++ b/src/Pure/library.scala	Fri Mar 07 14:37:25 2014 +0100
@@ -97,6 +97,9 @@
     else ""
   }
 
+  def plain_words(str: String): String =
+    space_explode('_', str).mkString(" ")
+
 
   /* strings */