# HG changeset patch
# User wenzelm
# Date 912341685 -3600
# Node ID 6ebbc9e7cc2033ebde2b37a164a6ca1e7e8fa9e3
# Parent  9481d0cfb86ed2682e83e90ccc4c02257bb7129f
added oct_char;

diff -r 9481d0cfb86e -r 6ebbc9e7cc20 src/Pure/term.ML
--- a/src/Pure/term.ML	Sun Nov 29 13:13:57 1998 +0100
+++ b/src/Pure/term.ML	Sun Nov 29 13:14:45 1998 +0100
@@ -125,6 +125,7 @@
   val maxidx_of_term: term -> int
   val read_radixint: int * string list -> int * string list
   val read_int: string list -> int * string list
+  val oct_char: string -> string
   val variant: string list -> string -> string
   val variantlist: string list * string list -> string list
   val variant_abs: string * typ * term -> string * term
@@ -690,7 +691,10 @@
 	      else (num, c::cs)
   in  scan(0,cs)  end;
 
-fun read_int cs = read_radixint(10,cs);
+fun read_int cs = read_radixint (10, cs);
+
+fun octal s = #1 (read_radixint (8, explode s));
+val oct_char = chr o octal;
 
 
 (*** Printing ***)