# HG changeset patch
# User wenzelm
# Date 963523180 -7200
# Node ID 1625c1f172b34d6ab646a1c78fcb62445e539076
# Parent  a7f3deedacdbefe0303f60bd7cc6f4114603c37a
added read_xnum;

diff -r a7f3deedacdb -r 1625c1f172b3 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Thu Jul 13 23:19:08 2000 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Thu Jul 13 23:19:40 2000 +0200
@@ -29,6 +29,7 @@
   val skolem: string -> string
   val dest_skolem: string -> string
   val read_nat: string -> int option
+  val read_xnum: string -> int
   val read_idents: string -> string list
 end;
 
@@ -342,6 +343,18 @@
   apsome (#1 o Term.read_int) (Scan.read Symbol.stopper scan_digits1 (Symbol.explode str));
 
 
+(* read_xnum *)
+
+fun read_xnum str =
+  let
+    val (sign, digs) =
+      (case Symbol.explode str of
+        "#" :: "-" :: cs => (~1, cs)
+      | "#" :: cs => (1, cs)
+      | _ => error ("Malformed number token: " ^ quote str));
+  in sign * #1 (Term.read_int digs) end;
+
+
 (* read_ident(s) *)
 
 fun read_idents str =