src/Pure/General/word.scala

--- a/src/Pure/General/word.scala	Sat Apr 26 13:34:10 2014 +0200
+++ b/src/Pure/General/word.scala	Sat Apr 26 13:50:25 2014 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/General/word.scala
     Author:     Makarius
 
-Support for plain text words.
+Support for words within Unicode text.
 */
 
 package isabelle
@@ -84,6 +84,6 @@
     explode(_ == sep, text)
 
   def explode(text: String): List[String] =
-    explode(Symbol.is_ascii_blank(_), text)
+    explode(Character.isWhitespace(_), text)
 }