* Renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token", in accordance to existing "float_token". Minor INCOMPATIBILITY. Note that in practice "num_const" etc. are mainly used instead. This refers to Isabelle/c7a13ce60161. Makarius