src/HOL/Tools/numeral.ML
changeset 55147 bce3dbc11f95
parent 54489 03ff4d1e6784
child 55148 7e1b7cb54114
     1.1 --- a/src/HOL/Tools/numeral.ML	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/HOL/Tools/numeral.ML	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -69,11 +69,11 @@
     1.4    let
     1.5      fun dest_numeral one' bit0' bit1' thm t =
     1.6        let
     1.7 -        fun dest_bit (IConst { name = c, ... }) = if c = bit0' then 0
     1.8 +        fun dest_bit (IConst { sym = Code_Symbol.Constant c, ... }) = if c = bit0' then 0
     1.9                else if c = bit1' then 1
    1.10                else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"
    1.11            | dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
    1.12 -        fun dest_num (IConst { name = c, ... }) = if c = one' then 1
    1.13 +        fun dest_num (IConst { sym = Code_Symbol.Constant c, ... }) = if c = one' then 1
    1.14                else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
    1.15            | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
    1.16            | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";