src/Pure/library.ML

--- a/src/Pure/library.ML	Mon Mar 10 22:08:51 2014 +0100
+++ b/src/Pure/library.ML	Mon Mar 10 22:14:53 2014 +0100
@@ -146,6 +146,7 @@
   val cat_lines: string list -> string
   val space_explode: string -> string -> string list
   val split_lines: string -> string list
+  val plain_words: string -> string
   val prefix_lines: string -> string -> string
   val prefix: string -> string -> string
   val suffix: string -> string -> string
@@ -745,6 +746,8 @@
 
 val split_lines = space_explode "\n";
 
+fun plain_words s = space_explode "_" s |> space_implode " ";
+
 fun prefix_lines "" txt = txt
   | prefix_lines prfx txt = txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines;