src/HOL/Num.thy
changeset 58410 6d46ad54a2ab
parent 58310 91ea607a34d8
child 58421 37cbbd8eb460
     1.1 --- a/src/HOL/Num.thy	Sun Sep 21 16:56:06 2014 +0200
     1.2 +++ b/src/HOL/Num.thy	Sun Sep 21 16:56:11 2014 +0200
     1.3 @@ -280,31 +280,14 @@
     1.4  syntax
     1.5    "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
     1.6  
     1.7 +ML_file "Tools/numeral.ML"
     1.8 +
     1.9  parse_translation {*
    1.10    let
    1.11 -    fun num_of_int n =
    1.12 -      if n > 0 then
    1.13 -        (case IntInf.quotRem (n, 2) of
    1.14 -          (0, 1) => Syntax.const @{const_syntax One}
    1.15 -        | (n, 0) => Syntax.const @{const_syntax Bit0} $ num_of_int n
    1.16 -        | (n, 1) => Syntax.const @{const_syntax Bit1} $ num_of_int n)
    1.17 -      else raise Match
    1.18 -    val numeral = Syntax.const @{const_syntax numeral}
    1.19 -    val uminus = Syntax.const @{const_syntax uminus}
    1.20 -    val one = Syntax.const @{const_syntax Groups.one}
    1.21 -    val zero = Syntax.const @{const_syntax Groups.zero}
    1.22      fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
    1.23            c $ numeral_tr [t] $ u
    1.24        | numeral_tr [Const (num, _)] =
    1.25 -          let
    1.26 -            val {value, ...} = Lexicon.read_xnum num;
    1.27 -          in
    1.28 -            if value = 0 then zero else
    1.29 -            if value > 0
    1.30 -            then numeral $ num_of_int value
    1.31 -            else if value = ~1 then uminus $ one
    1.32 -            else uminus $ (numeral $ num_of_int (~ value))
    1.33 -          end
    1.34 +          (Numeral.mk_number_syntax o #value o Lexicon.read_xnum) num
    1.35        | numeral_tr ts = raise TERM ("numeral_tr", ts);
    1.36    in [(@{syntax_const "_Numeral"}, K numeral_tr)] end
    1.37  *}
    1.38 @@ -334,8 +317,6 @@
    1.39    end
    1.40  *}
    1.41  
    1.42 -ML_file "Tools/numeral.ML"
    1.43 -
    1.44  
    1.45  subsection {* Class-specific numeral rules *}
    1.46