moved read_int etc. to library.ML; added type 'arity';
authorwenzelm
Sat May 29 15:05:02 2004 +0200 (2004-05-29)
changeset 14829cfa5fe01a7b7
parent 14828 15d12761ba54
child 14830 faa4865ba1ce
moved read_int etc. to library.ML; added type 'arity';
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Sat May 29 15:03:59 2004 +0200
     1.2 +++ b/src/Pure/term.ML	Sat May 29 15:05:02 2004 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4    type indexname
     1.5    type class
     1.6    type sort
     1.7 +  type arity
     1.8    datatype typ =
     1.9      Type  of string * typ list |
    1.10      TFree of string * sort |
    1.11 @@ -128,9 +129,6 @@
    1.12    val maxidx_of_typs: typ list -> int
    1.13    val maxidx_of_term: term -> int
    1.14    val maxidx_of_terms: term list -> int
    1.15 -  val read_radixint: int * string list -> int * string list
    1.16 -  val read_int: string list -> int * string list
    1.17 -  val oct_char: string -> string
    1.18    val variant: string list -> string -> string
    1.19    val variantlist: string list * string list -> string list
    1.20    val variant_abs: string * typ * term -> string * term
    1.21 @@ -205,6 +203,7 @@
    1.22  (* Types are classified by sorts. *)
    1.23  type class = string;
    1.24  type sort  = class list;
    1.25 +type arity = string * sort list * sort;
    1.26  
    1.27  (* The sorts attached to TFrees and TVars specify the sort of that variable *)
    1.28  datatype typ = Type  of string * typ list
    1.29 @@ -719,22 +718,6 @@
    1.30        | check _ = ();
    1.31    in check typ; typ end;
    1.32  
    1.33 -(*read a numeral of the given radix, normally 10*)
    1.34 -fun read_radixint (radix: int, cs) : int * string list =
    1.35 -  let val zero = ord"0"
    1.36 -      val limit = zero+radix
    1.37 -      fun scan (num,[]) = (num,[])
    1.38 -        | scan (num, c::cs) =
    1.39 -              if  zero <= ord c  andalso  ord c < limit
    1.40 -              then scan(radix*num + ord c - zero, cs)
    1.41 -              else (num, c::cs)
    1.42 -  in  scan(0,cs)  end;
    1.43 -
    1.44 -fun read_int cs = read_radixint (10, cs);
    1.45 -
    1.46 -fun octal s = #1 (read_radixint (8, explode s));
    1.47 -val oct_char = chr o octal;
    1.48 -
    1.49  
    1.50  (*** Printing ***)
    1.51