# HG changeset patch
# User wenzelm
# Date 1154550427 -7200
# Node ID bf9101cc43852dc9a8d33f1d765fb0b66c3cf433
# Parent  3b3da376d94d1c4fdf10733f7ba7fefce4c6aa06
renamed Syntax.indexname to Syntax.read_indexname;
added read_int (not Int.fromString, which admits ~ syntax of ML);

diff -r 3b3da376d94d -r bf9101cc4385 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Wed Aug 02 22:27:06 2006 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Wed Aug 02 22:27:07 2006 +0200
@@ -23,13 +23,14 @@
   val scan_bin: string list -> string * string list
   val string_of_vname: indexname -> string
   val string_of_vname': indexname -> string
-  val indexname: string -> indexname
+  val read_indexname: string -> indexname
   val read_var: string -> term
   val read_variable: string -> indexname option
   val const: string -> term
   val free: string -> term
   val var: indexname -> term
   val read_nat: string -> int option
+  val read_int: string -> int option
   val read_xnum: string -> IntInf.int
   val read_idents: string -> string list
   val fixedN: string
@@ -328,10 +329,10 @@
 
 (* indexname *)
 
-fun indexname cs =
-  (case Scan.read Symbol.stopper scan_indexname (Symbol.explode cs) of
+fun read_indexname s =
+  (case Scan.read Symbol.stopper scan_indexname (Symbol.explode s) of
     SOME xi => xi
-  | _ => error ("Lexical error in variable name: " ^ quote cs));
+  | _ => error ("Lexical error in variable name: " ^ quote s));
 
 
 (* read_var *)
@@ -361,11 +362,24 @@
 val fixedN = "\\<^fixed>";
 
 
-(* read_nat *)
+(* read numbers *)
+
+local
+
+fun nat cs =
+  Option.map (#1 o Library.read_int)
+    (Scan.read Symbol.stopper scan_digits1 cs);
 
-fun read_nat s =
-  Option.map (#1 o Library.read_int)
-    (Scan.read Symbol.stopper scan_digits1 (Symbol.explode s));
+in
+
+val read_nat = nat o Symbol.explode;
+
+fun read_int s =
+  (case Symbol.explode s of
+    "-" :: cs => Option.map ~ (nat cs)
+  | cs => nat cs);
+
+end;
 
 
 (* read_xnum: hex/bin/decimal *)