added numeral, which supercedes num, xnum, float;
renamed xstr to inner_string;

--- a/src/Pure/General/markup.ML	Fri Jan 02 19:30:12 2009 +0100
+++ b/src/Pure/General/markup.ML	Fri Jan 02 19:38:13 2009 +0100
@@ -52,11 +52,9 @@
   val skolemN: string val skolem: T
   val boundN: string val bound: T
   val varN: string val var: T
-  val numN: string val num: T
-  val floatN: string val float: T
-  val xnumN: string val xnum: T
-  val xstrN: string val xstr: T
+  val numeralN: string val numeral: T
   val literalN: string val literal: T
+  val inner_stringN: string val inner_string: T
   val inner_commentN: string val inner_comment: T
   val sortN: string val sort: T
   val typN: string val typ: T
@@ -203,11 +201,9 @@
 val (skolemN, skolem) = markup_elem "skolem";
 val (boundN, bound) = markup_elem "bound";
 val (varN, var) = markup_elem "var";
-val (numN, num) = markup_elem "num";
-val (floatN, float) = markup_elem "float";
-val (xnumN, xnum) = markup_elem "xnum";
-val (xstrN, xstr) = markup_elem "xstr";
+val (numeralN, numeral) = markup_elem "numeral";
 val (literalN, literal) = markup_elem "literal";
+val (inner_stringN, inner_string) = markup_elem "inner_string";
 val (inner_commentN, inner_comment) = markup_elem "inner_comment";
 
 val (sortN, sort) = markup_elem "sort";

--- a/src/Pure/Isar/proof_context.ML	Fri Jan 02 19:30:12 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Jan 02 19:38:13 2009 +0100
@@ -408,9 +408,8 @@
    ("free", free_or_skolem),
    ("bound", plain_markup Markup.bound),
    ("var", var_or_skolem),
-   ("num", plain_markup Markup.num),
-   ("xnum", plain_markup Markup.xnum),
-   ("xstr", plain_markup Markup.xstr)];
+   ("numeral", plain_markup Markup.numeral),
+   ("inner_string", plain_markup Markup.inner_string)];
 
 in val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans)) end;
 

--- a/src/Pure/Syntax/lexicon.ML	Fri Jan 02 19:30:12 2009 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Fri Jan 02 19:38:13 2009 +0100
@@ -169,10 +169,10 @@
   | VarSy       => Markup.var
   | TFreeSy     => Markup.tfree
   | TVarSy      => Markup.tvar
-  | NumSy       => Markup.num
-  | FloatSy     => Markup.float
-  | XNumSy      => Markup.xnum
-  | StrSy       => Markup.xstr
+  | NumSy       => Markup.numeral
+  | FloatSy     => Markup.numeral
+  | XNumSy      => Markup.numeral
+  | StrSy       => Markup.inner_string
   | Space       => Markup.none
   | Comment     => Markup.inner_comment
   | EOF         => Markup.none;

--- a/src/Pure/Syntax/syn_ext.ML	Fri Jan 02 19:30:12 2009 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Fri Jan 02 19:38:13 2009 +0100
@@ -379,7 +379,7 @@
 
 fun stamp_trfun s (c, f) = (c, (f, s));
 fun mk_trfun tr = stamp_trfun (stamp ()) tr;
-fun eq_trfun ((_, s1:stamp), (_, s2)) = s1 = s2;
+fun eq_trfun ((_, s1: stamp), (_, s2)) = s1 = s2;
 
 
 (* token translations *)
@@ -387,7 +387,7 @@
 fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
 
 val standard_token_classes =
-  ["class", "tfree", "tvar", "free", "bound", "var", "num", "float", "xnum", "xstr"];
+  ["class", "tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"];
 
 val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes;