src/Pure/General/word.scala

--- a/src/Pure/General/word.scala	Tue Apr 29 16:14:27 2014 +0200
+++ b/src/Pure/General/word.scala	Tue Apr 29 20:40:44 2014 +0200
@@ -27,6 +27,8 @@
       }
     }
 
+  def codepoint(c: Int): String = new String(Array(c), 0, 1)
+
 
   /* case */