# HG changeset patch
# User wenzelm
# Date 889456172 -3600
# Node ID 92e12a04dca7d75633d93563a3809cf70786432d
# Parent  2e47ea2c61093fb4ee736ba7b23fb051236c3a2f
tuned some names;

diff -r 2e47ea2c6109 -r 92e12a04dca7 src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Mar 09 16:09:06 1998 +0100
+++ b/src/Pure/term.ML	Mon Mar 09 16:09:32 1998 +0100
@@ -122,8 +122,8 @@
   val maxidx_of_typ: typ -> int
   val maxidx_of_typs: typ list -> int
   val maxidx_of_term: term -> int
-  val scan_radixint: int * string list -> int * string list
-  val scan_int: string list -> int * string list
+  val read_radixint: int * string list -> int * string list
+  val read_int: string list -> int * string list
   val variant: string list -> string -> string
   val variantlist: string list * string list -> string list
   val variant_abs: string * typ * term -> string * term
@@ -674,8 +674,8 @@
 (*Dummy type for parsing and printing.  Will be replaced during type inference. *)
 val dummyT = Type("dummy",[]);
 
-(*scan a numeral of the given radix, normally 10*)
-fun scan_radixint (radix: int, cs) : int * string list =
+(*read a numeral of the given radix, normally 10*)
+fun read_radixint (radix: int, cs) : int * string list =
   let val zero = ord"0"
       val limit = zero+radix
       fun scan (num,[]) = (num,[])
@@ -685,7 +685,7 @@
 	      else (num, c::cs)
   in  scan(0,cs)  end;
 
-fun scan_int cs = scan_radixint(10,cs);
+fun read_int cs = read_radixint(10,cs);
 
 
 (*** Printing ***)