src/HOL/Tools/numeral.ML
changeset 48072 ace701efe203
parent 47108 2a1953f0d20d
child 51314 eac4bb5adbf9
     1.1 --- a/src/HOL/Tools/numeral.ML	Mon Jun 04 12:55:54 2012 +0200
     1.2 +++ b/src/HOL/Tools/numeral.ML	Tue Jun 05 07:05:56 2012 +0200
     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 (c, _)) = if c = bit0' then 0
     1.8 +        fun dest_bit (IConst { name = 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 (c, _)) = if c = one' then 1
    1.13 +        fun dest_num (IConst { name = 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";