src/HOL/Num.thy
changeset 62597 b3f2b8c906a6
parent 62481 b5d8e57826df
child 63654 f90e3926e627
     1.1 --- a/src/HOL/Num.thy	Fri Mar 11 17:20:14 2016 +0100
     1.2 +++ b/src/HOL/Num.thy	Sat Mar 12 22:04:52 2016 +0100
     1.3 @@ -297,12 +297,9 @@
     1.4  
     1.5  typed_print_translation \<open>
     1.6    let
     1.7 -    fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n
     1.8 -      | dest_num (Const (@{const_syntax Bit1}, _) $ n) = 2 * dest_num n + 1
     1.9 -      | dest_num (Const (@{const_syntax One}, _)) = 1;
    1.10      fun num_tr' ctxt T [n] =
    1.11        let
    1.12 -        val k = dest_num n;
    1.13 +        val k = Numeral.dest_num_syntax n;
    1.14          val t' =
    1.15            Syntax.const @{syntax_const "_Numeral"} $
    1.16              Syntax.free (string_of_int k);