discontinued old "xnum" token category;
simplified Lexicon.read_num, Lexicon.read_float: no sign here;
express ZF numerals via "num" with mixfix grammar;
recovered printing of ZF numerals: "one" is abbreviation;

--- a/NEWS	Mon Sep 22 17:07:18 2014 +0200
+++ b/NEWS	Mon Sep 22 21:28:57 2014 +0200
@@ -25,6 +25,10 @@
 of numeral signs, particulary in expressions involving infix syntax like
 "(- 1) ^ n".
 
+* Old inner token category "xnum" has been discontinued.  Potential
+INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num"
+token category instead.
+
 
 *** HOL ***
 

--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Sep 22 17:07:18 2014 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Sep 22 21:28:57 2014 +0200
@@ -601,7 +601,6 @@
     @{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\
     @{syntax_def (inner) num_token} & = & @{syntax_ref nat} \\
     @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
-    @{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text "  |  "}@{verbatim "#-"}@{syntax_ref nat} \\
     @{syntax_def (inner) str_token} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
     @{syntax_def (inner) string_token} & = & @{verbatim "\""} @{text "\<dots>"} @{verbatim "\""} \\
     @{syntax_def (inner) cartouche} & = & @{verbatim "\<open>"} @{text "\<dots>"} @{verbatim "\<close>"} \\
@@ -609,17 +608,15 @@
   \end{center}
 
   The token categories @{syntax (inner) num_token}, @{syntax (inner)
-  float_token}, @{syntax (inner) xnum_token}, @{syntax (inner)
-  str_token}, @{syntax (inner) string_token}, and @{syntax (inner)
-  cartouche} are not used in Pure. Object-logics may implement
-  numerals and string literals by adding appropriate syntax
-  declarations, together with some translation functions (e.g.\ see
-  @{file "~~/src/HOL/Tools/string_syntax.ML"}).
+  float_token}, @{syntax (inner) str_token}, @{syntax (inner) string_token},
+  and @{syntax (inner) cartouche} are not used in Pure. Object-logics may
+  implement numerals and string literals by adding appropriate syntax
+  declarations, together with some translation functions (e.g.\ see @{file
+  "~~/src/HOL/Tools/string_syntax.ML"}).
 
-  The derived categories @{syntax_def (inner) num_const}, @{syntax_def
-  (inner) float_const}, and @{syntax_def (inner) xnum_const} provide
-  robust access to the respective tokens: the syntax tree holds a
-  syntactic constant instead of a free variable.
+  The derived categories @{syntax_def (inner) num_const}, and @{syntax_def
+  (inner) float_const}, provide robust access to the respective tokens: the
+  syntax tree holds a syntactic constant instead of a free variable.
 *}
 
 

--- a/src/HOL/Num.thy	Mon Sep 22 17:07:18 2014 +0200
+++ b/src/HOL/Num.thy	Mon Sep 22 21:28:57 2014 +0200
@@ -287,7 +287,7 @@
     fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
           c $ numeral_tr [t] $ u
       | numeral_tr [Const (num, _)] =
-          (Numeral.mk_number_syntax o #value o Lexicon.read_xnum) num
+          (Numeral.mk_number_syntax o #value o Lexicon.read_num) num
       | numeral_tr ts = raise TERM ("numeral_tr", ts);
   in [(@{syntax_const "_Numeral"}, K numeral_tr)] end
 *}

--- a/src/Pure/Syntax/lexicon.ML	Mon Sep 22 17:07:18 2014 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Mon Sep 22 21:28:57 2014 +0200
@@ -16,7 +16,6 @@
   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
@@ -25,7 +24,7 @@
   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
@@ -52,7 +51,7 @@
   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
@@ -99,9 +98,9 @@
 
 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;
@@ -118,7 +117,7 @@
 
 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;
 
@@ -151,7 +150,6 @@
   ("tvar", TVarSy),
   ("num_token", NumSy),
   ("float_token", FloatSy),
-  ("xnum_token", XNumSy),
   ("str_token", StrSy),
   ("string_token", StringSy),
   ("cartouche", Cartouche)];
@@ -172,7 +170,6 @@
   | TVarSy => Markup.tvar
   | NumSy => Markup.numeral
   | FloatSy => Markup.numeral
-  | XNumSy => Markup.numeral
   | StrSy => Markup.inner_string
   | StringSy => Markup.inner_string
   | Cartouche => Markup.inner_cartouche
@@ -263,16 +260,12 @@
       (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;
 
@@ -378,7 +371,7 @@
 end;
 
 
-(* read_xnum: hex/bin/decimal *)
+(* read_num: hex/bin/decimal *)
 
 local
 
@@ -400,34 +393,30 @@
 
 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;
 

--- a/src/Pure/pure_thy.ML	Mon Sep 22 17:07:18 2014 +0200
+++ b/src/Pure/pure_thy.ML	Mon Sep 22 21:28:57 2014 +0200
@@ -70,8 +70,8 @@
     (map (fn name => Binding.make (name, @{here}))
       (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
         "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
-        "any", "prop'", "num_const", "float_const", "xnum_const", "num_position",
-        "float_position", "xnum_position", "index", "struct", "tid_position",
+        "any", "prop'", "num_const", "float_const", "num_position",
+        "float_position", "index", "struct", "tid_position",
         "tvar_position", "id_position", "longid_position", "var_position",
         "str_position", "string_position", "cartouche_position", "type_name",
         "class_name"]))
@@ -142,10 +142,8 @@
     ("_strip_positions", typ "'a", NoSyn),
     ("_position",   typ "num_token => num_position",   Delimfix "_"),
     ("_position",   typ "float_token => float_position", Delimfix "_"),
-    ("_position",   typ "xnum_token => xnum_position", Delimfix "_"),
     ("_constify",   typ "num_position => num_const",   Delimfix "_"),
     ("_constify",   typ "float_position => float_const", Delimfix "_"),
-    ("_constify",   typ "xnum_position => xnum_const", Delimfix "_"),
     ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
     ("_indexdefault", typ "index",                     Delimfix ""),
     ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),

--- a/src/ZF/Bin.thy	Mon Sep 22 17:07:18 2014 +0200
+++ b/src/ZF/Bin.thy	Mon Sep 22 21:28:57 2014 +0200
@@ -101,10 +101,23 @@
                                  NCons(bin_mult(v,w),0))"
 
 syntax
-  "_Int"    :: "xnum_token => i"        ("_")
+  "_Int0" :: i  ("#()0")
+  "_Int1" :: i  ("#()1")
+  "_Int2" :: i  ("#()2")
+  "_Neg_Int1" :: i  ("#-()1")
+  "_Neg_Int2" :: i  ("#-()2")
+translations
+  "#0" \<rightleftharpoons> "CONST integ_of(CONST Pls)"
+  "#1" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1)"
+  "#2" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1 BIT 0)"
+  "#-1" \<rightleftharpoons> "CONST integ_of(CONST Min)"
+  "#-2" \<rightleftharpoons> "CONST integ_of(CONST Min BIT 0)"
+
+syntax
+  "_Int" :: "num_token => i"  ("#_" 1000)
+  "_Neg_Int" :: "num_token => i"  ("#-_" 1000)
 
 ML_file "Tools/numeral_syntax.ML"
-setup Numeral_Syntax.setup
 
 
 declare bin.intros [simp,TC]

--- a/src/ZF/Tools/numeral_syntax.ML	Mon Sep 22 17:07:18 2014 +0200
+++ b/src/ZF/Tools/numeral_syntax.ML	Mon Sep 22 21:28:57 2014 +0200
@@ -8,7 +8,6 @@
 sig
   val make_binary: int -> int list
   val dest_binary: int list -> int
-  val setup: theory -> theory
 end;
 
 structure Numeral_Syntax: NUMERAL_SYNTAX =
@@ -21,6 +20,7 @@
   | mk_bit _ = raise Fail "mk_bit";
 
 fun dest_bit (Const (@{const_syntax zero}, _)) = 0
+  | dest_bit (Const (@{const_syntax one}, _)) = 1
   | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax zero}, _)) = 1
   | dest_bit _ = raise Match;
 
@@ -58,28 +58,34 @@
 fun show_int t =
   let
     val rev_digs = bin_of t;
-    val (sign, zs) =
+    val (c, zs) =
       (case rev rev_digs of
-         ~1 :: bs => ("-", prefix_len (equal 1) bs)
-      | bs => ("",  prefix_len (equal 0) bs));
+         ~1 :: bs => (@{syntax_const "_Neg_Int"}, prefix_len (equal 1) bs)
+      | bs => (@{syntax_const "_Int"},  prefix_len (equal 0) bs));
     val num = string_of_int (abs (dest_binary rev_digs));
-  in
-    "#" ^ sign ^ implode (replicate zs "0") ^ num
-  end;
+  in (c, implode (replicate zs "0") ^ num) end;
 
 
 (* translation of integer constant tokens to and from binary *)
 
-fun int_tr [t as Free (str, _)] =
-      Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Lexicon.read_xnum str))
+fun int_tr [Free (s, _)] =
+      Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Lexicon.read_num s))
   | int_tr ts = raise TERM ("int_tr", ts);
 
-fun int_tr' [t] = Syntax.const @{syntax_const "_Int"} $ Syntax.free (show_int t)
-  | int_tr' _ = raise Match;
-
+fun neg_int_tr [Free (s, _)] =
+      Syntax.const @{const_syntax integ_of} $ mk_bin (~ (#value (Lexicon.read_num s)))
+  | neg_int_tr ts = raise TERM ("neg_int_tr", ts);
 
-val setup =
- Sign.parse_translation [(@{syntax_const "_Int"}, K int_tr)] #>
- Sign.print_translation [(@{const_syntax integ_of}, K int_tr')];
+fun integ_of_tr' [t] =
+      let val (c, s) = show_int t
+      in Syntax.const c $ Syntax.free s end
+  | integ_of_tr' _ = raise Match;
+
+val _ = Theory.setup
+ (Sign.parse_translation
+   [(@{syntax_const "_Int"}, K int_tr),
+    (@{syntax_const "_Neg_Int"}, K neg_int_tr)] #>
+  Sign.print_translation
+   [(@{const_syntax integ_of}, K integ_of_tr')]);
 
 end;