--- a/src/Pure/library.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/library.ML Sat Nov 20 00:53:26 2010 +0100
@@ -669,7 +669,7 @@
val read_int = read_radix_int 10;
-fun oct_char s = chr (#1 (read_radix_int 8 (explode s)));
+fun oct_char s = chr (#1 (read_radix_int 8 (raw_explode s)));