src/HOL/ex/Numeral.thy

   then (range_type (fastype_of u), dest_num t)
   else raise TERM ("dest_numeral", [u, t]);
 *}
 
 syntax
-  "_Numerals" :: "xnum \<Rightarrow> 'a"    ("_")
+  "_Numerals" :: "xnum_token \<Rightarrow> 'a"    ("_")
 
 parse_translation {*
 let
   fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)
      of (0, 1) => Const (@{const_name One}, dummyT)