src/Pure/library.ML
changeset 40627 becf5d5187cc
parent 40564 6827505e96e1
child 40721 e5089e903e39
child 40731 4e60c7348096
     1.1 --- a/src/Pure/library.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/Pure/library.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -669,7 +669,7 @@
     1.4  
     1.5  val read_int = read_radix_int 10;
     1.6  
     1.7 -fun oct_char s = chr (#1 (read_radix_int 8 (explode s)));
     1.8 +fun oct_char s = chr (#1 (read_radix_int 8 (raw_explode s)));
     1.9  
    1.10  
    1.11