src/HOL/ex/Numeral.thy

       | (n, 0) => Const (@{const_name Dig0}, dummyT) $ num_of_int n
       | (n, 1) => Const (@{const_name Dig1}, dummyT) $ num_of_int n
     else raise Match;
   fun numeral_tr [Free (num, _)] =
         let
-          val {leading_zeros, value, ...} = Syntax.read_xnum num;
+          val {leading_zeros, value, ...} = Lexicon.read_xnum num;
           val _ = leading_zeros = 0 andalso value > 0
             orelse error ("Bad numeral: " ^ num);
         in Const (@{const_name of_num}, @{typ num} --> dummyT) $ num_of_int value end
     | numeral_tr ts = raise TERM ("numeral_tr", ts);
 in [(@{syntax_const "_Numerals"}, numeral_tr)] end