src/HOL/Num.thy
changeset 55974 c835a9379026
parent 55534 b18bdcbda41b
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Num.thy	Fri Mar 07 11:41:25 2014 +0100
     1.2 +++ b/src/HOL/Num.thy	Fri Mar 07 11:46:26 2014 +0100
     1.3 @@ -285,14 +285,14 @@
     1.4      fun num_of_int n =
     1.5        if n > 0 then
     1.6          (case IntInf.quotRem (n, 2) of
     1.7 -          (0, 1) => Syntax.const @{const_name One}
     1.8 -        | (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
     1.9 -        | (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n)
    1.10 +          (0, 1) => Syntax.const @{const_syntax One}
    1.11 +        | (n, 0) => Syntax.const @{const_syntax Bit0} $ num_of_int n
    1.12 +        | (n, 1) => Syntax.const @{const_syntax Bit1} $ num_of_int n)
    1.13        else raise Match
    1.14 -    val numeral = Syntax.const @{const_name numeral}
    1.15 -    val uminus = Syntax.const @{const_name uminus}
    1.16 -    val one = Syntax.const @{const_name Groups.one}
    1.17 -    val zero = Syntax.const @{const_name Groups.zero}
    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 @@ -303,10 +303,10 @@
    1.26              if value > 0
    1.27              then numeral $ num_of_int value
    1.28              else if value = ~1 then uminus $ one
    1.29 -            else uminus $ (numeral $ num_of_int (~value))
    1.30 +            else uminus $ (numeral $ num_of_int (~ value))
    1.31            end
    1.32        | numeral_tr ts = raise TERM ("numeral_tr", ts);
    1.33 -  in [("_Numeral", K numeral_tr)] end
    1.34 +  in [(@{syntax_const "_Numeral"}, K numeral_tr)] end
    1.35  *}
    1.36  
    1.37  typed_print_translation {*