src/Pure/General/word.scala

--- a/src/Pure/General/word.scala	Sun Dec 22 14:21:39 2024 +0100
+++ b/src/Pure/General/word.scala	Mon Dec 23 14:09:43 2024 +0100
@@ -76,6 +76,8 @@
   def explode(text: String): List[String] =
     explode(Character.isWhitespace _, text)
 
+  def informal(text: String): String = implode(explode('_', text))
+
 
   /* brackets */