src/Pure/System/standard_system.scala

--- a/src/Pure/System/standard_system.scala	Tue Aug 10 18:23:12 2010 +0200
+++ b/src/Pure/System/standard_system.scala	Tue Aug 10 18:24:16 2010 +0200
@@ -19,9 +19,13 @@
 
 object Standard_System
 {
+  /* UTF-8 charset */
+
   val charset = "UTF-8"
   def codec(): Codec = Codec(charset)
 
+  def string_bytes(s: String): Array[Byte] = s.getBytes(charset)
+
 
   /* permissive UTF-8 decoding */