src/HOL/Tools/numeral_syntax.ML
changeset 26086 3c243098b64a
parent 25919 8b1c0d434824
child 29316 0a7fcdd77f4b
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Sat Feb 16 16:52:09 2008 +0100
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Sun Feb 17 06:49:53 2008 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4  fun mk_bin num =
     1.5    let
     1.6      val {leading_zeros = z, value, ...} = Syntax.read_xnum num;
     1.7 -    fun bit b bs = Syntax.const @{const_name Int.Bit} $ bs $ HOLogic.mk_bit b;
     1.8 +    fun bit b bs = HOLogic.mk_bit b $ bs;
     1.9      fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const @{const_name Int.Pls})
    1.10        | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const @{const_name Int.Min})
    1.11        | mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end;
    1.12 @@ -39,15 +39,10 @@
    1.13  
    1.14  local
    1.15  
    1.16 -fun dest_bit (Const (@{const_syntax Int.bit.B0}, _)) = 0
    1.17 -  | dest_bit (Const (@{const_syntax Int.bit.B1}, _)) = 1
    1.18 -  | dest_bit (Const ("bit.B0", _)) = 0
    1.19 -  | dest_bit (Const ("bit.B1", _)) = 1
    1.20 -  | dest_bit _ = raise Match;
    1.21 -
    1.22  fun dest_bin (Const (@{const_syntax "Int.Pls"}, _)) = []
    1.23    | dest_bin (Const (@{const_syntax "Int.Min"}, _)) = [~1]
    1.24 -  | dest_bin (Const (@{const_syntax "Int.Bit"}, _) $ bs $ b) = dest_bit b :: dest_bin bs
    1.25 +  | dest_bin (Const (@{const_syntax "Int.Bit0"}, _) $ bs) = 0 :: dest_bin bs
    1.26 +  | dest_bin (Const (@{const_syntax "Int.Bit1"}, _) $ bs) = 1 :: dest_bin bs
    1.27    | dest_bin _ = raise Match;
    1.28  
    1.29  fun leading _ [] = 0