Symbol.explode as in ML;

--- a/src/Pure/General/symbol.scala	Sat Sep 17 16:00:54 2011 +0200
+++ b/src/Pure/General/symbol.scala	Sat Sep 17 16:19:40 2011 +0200
@@ -115,6 +115,8 @@
       }
     }
 
+  def explode(text: CharSequence): List[Symbol] = iterator(text).toList
+
 
   /* decoding offsets */