src/HOL/Tools/numeral_syntax.ML

   let
     fun bit b bs = HOLogic.mk_bit b $ bs;
     fun mk 0 = Syntax.const @{const_name Int.Pls}
       | mk ~1 = Syntax.const @{const_name Int.Min}
       | mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end;
-  in mk (#value (Syntax.read_xnum num)) end;
+  in mk (#value (Lexicon.read_xnum num)) end;
 
 in
 
 fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] =
       Syntax.const @{const_syntax Int.number_of} $ mk_bin num