src/Pure/Syntax/lexicon.ML

   end
   val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val scan_nat: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
-  val scan_int: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val scan_float: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val scan_hex: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val is_tid: string -> bool
   datatype token_kind =
     Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy |
-    FloatSy | XNumSy | StrSy | StringSy | Cartouche | Space | Comment | EOF
+    FloatSy | StrSy | StringSy | Cartouche | Space | Comment | EOF
   datatype token = Token of token_kind * string * Position.range
   val str_of_token: token -> string
   val pos_of_token: token -> Position.T
   val is_proper: token -> bool
   val mk_eof: Position.T -> token

   val read_indexname: string -> indexname
   val read_var: string -> term
   val read_variable: string -> indexname option
   val read_nat: string -> int option
   val read_int: string -> int option
-  val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
+  val read_num: string -> {radix: int, leading_zeros: int, value: int}
   val read_float: string -> {mant: int, exp: int}
   val mark_class: string -> string val unmark_class: string -> string
   val mark_type: string -> string val unmark_type: string -> string
   val mark_const: string -> string val unmark_const: string -> string
   val mark_fixed: string -> string val unmark_fixed: string -> string

 val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
 val scan_tid = $$$ "'" @@@ scan_id;
 
 val scan_nat = Scan.many1 (Symbol.is_digit o Symbol_Pos.symbol);
 val scan_float = scan_nat @@@ $$$ "." @@@ scan_nat;
-val scan_int = $$$ "-" @@@ scan_nat || scan_nat;
 val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);
 val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1");
+val scan_num = scan_hex || scan_bin || scan_nat;
 
 val scan_id_nat = scan_id @@@ Scan.optional ($$$ "." @@@ scan_nat) [];
 val scan_var = $$$ "?" @@@ scan_id_nat;
 val scan_tvar = $$$ "?" @@@ $$$ "'" @@@ scan_id_nat;
 

 
 (** datatype token **)
 
 datatype token_kind =
   Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy |
-  FloatSy | XNumSy | StrSy | StringSy | Cartouche | Space | Comment | EOF;
+  FloatSy | StrSy | StringSy | Cartouche | Space | Comment | EOF;
 
 datatype token = Token of token_kind * string * Position.range;
 
 fun str_of_token (Token (_, s, _)) = s;
 fun pos_of_token (Token (_, _, (pos, _))) = pos;

   ("var", VarSy),
   ("tid", TFreeSy),
   ("tvar", TVarSy),
   ("num_token", NumSy),
   ("float_token", FloatSy),
-  ("xnum_token", XNumSy),
   ("str_token", StrSy),
   ("string_token", StringSy),
   ("cartouche", Cartouche)];
 
 val terminals = map #1 terminal_kinds;

 val token_kind_markup =
  fn TFreeSy => Markup.tfree
   | TVarSy => Markup.tvar
   | NumSy => Markup.numeral
   | FloatSy => Markup.numeral
-  | XNumSy => Markup.numeral
   | StrSy => Markup.inner_string
   | StringSy => Markup.inner_string
   | Cartouche => Markup.inner_cartouche
   | Comment => Markup.inner_comment
   | _ => Markup.empty;

   let
     val scan_xid =
       (if xids then $$$ "_" @@@ scan_id || scan_id else scan_id) ||
       $$$ "_" @@@ $$$ "_";
 
-    val scan_num_unsigned = scan_hex || scan_bin || scan_nat;
-    val scan_num_signed = scan_hex || scan_bin || scan_int;
-
     val scan_val =
       scan_tvar >> token TVarSy ||
       scan_var >> token VarSy ||
       scan_tid >> token TFreeSy ||
       scan_float >> token FloatSy ||
-      scan_num_unsigned >> token NumSy ||
-      $$$ "#" @@@ scan_num_signed >> token XNumSy ||
+      scan_num >> token NumSy ||
       scan_longid >> token LongIdentSy ||
       scan_xid >> token IdentSy;
 
     val scan_lit = Scan.literal lex >> token Literal;
 

   | cs => nat cs);
 
 end;
 
 
-(* read_xnum: hex/bin/decimal *)
+(* read_num: hex/bin/decimal *)
 
 local
 
 val ten = ord "0" + 10;
 val a = ord "a";

   | leading_zeros ("0" :: cs) = 1 + leading_zeros cs
   | leading_zeros _ = 0;
 
 in
 
-fun read_xnum str =
+fun read_num str =
   let
-    val (sign, radix, digs) =
-      (case Symbol.explode (perhaps (try (unprefix "#")) str) of
-        "0" :: "x" :: cs => (1, 16, map remap_hex cs)
-      | "0" :: "b" :: cs => (1, 2, cs)
-      | "-" :: cs => (~1, 10, cs)
-      | cs => (1, 10, cs));
+    val (radix, digs) =
+      (case Symbol.explode str of
+        "0" :: "x" :: cs => (16, map remap_hex cs)
+      | "0" :: "b" :: cs => (2, cs)
+      | cs => (10, cs));
   in
    {radix = radix,
     leading_zeros = leading_zeros digs,
-    value = sign * #1 (Library.read_radix_int radix digs)}
+    value = #1 (Library.read_radix_int radix digs)}
   end;
 
 end;
 
 fun read_float str =
   let
-    val (sign, cs) =
-      (case Symbol.explode str of
-        "-" :: cs => (~1, cs)
-      | cs => (1, cs));
+    val cs = Symbol.explode str;
     val (intpart, fracpart) =
       (case take_prefix Symbol.is_digit cs of
         (intpart, "." :: fracpart) => (intpart, fracpart)
       | _ => raise Fail "read_float");
   in
-   {mant = sign * #1 (Library.read_int (intpart @ fracpart)),
+   {mant = #1 (Library.read_int (intpart @ fracpart)),
     exp = length fracpart}
   end;
 
 
 (* marked logical entities *)