src/HOL/Num.thy
changeset 58421 37cbbd8eb460
parent 58410 6d46ad54a2ab
child 58512 dc4d76dfa8f0
     1.1 --- a/src/HOL/Num.thy	Mon Sep 22 17:07:18 2014 +0200
     1.2 +++ b/src/HOL/Num.thy	Mon Sep 22 21:28:57 2014 +0200
     1.3 @@ -287,7 +287,7 @@
     1.4      fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
     1.5            c $ numeral_tr [t] $ u
     1.6        | numeral_tr [Const (num, _)] =
     1.7 -          (Numeral.mk_number_syntax o #value o Lexicon.read_xnum) num
     1.8 +          (Numeral.mk_number_syntax o #value o Lexicon.read_num) num
     1.9        | numeral_tr ts = raise TERM ("numeral_tr", ts);
    1.10    in [(@{syntax_const "_Numeral"}, K numeral_tr)] end
    1.11  *}