src/HOL/Tools/numeral_syntax.ML
changeset 22997 d4f3b015b50b
parent 21821 7fa19d17f488
child 24630 351a308ab58d
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Thu May 17 19:49:21 2007 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Thu May 17 19:49:40 2007 +0200
     1.3 @@ -20,16 +20,16 @@
     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>Numeral.Bit" $ bs $ HOLogic.mk_bit b;
     1.8 -    fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const "\\<^const>Numeral.Pls")
     1.9 -      | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const "\\<^const>Numeral.Min")
    1.10 +    fun bit b bs = Syntax.const @{const_name Numeral.Bit} $ bs $ HOLogic.mk_bit b;
    1.11 +    fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const @{const_name Numeral.Pls})
    1.12 +      | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const @{const_name Numeral.Min})
    1.13        | mk i = let val (q, r) = IntInf.divMod (i, 2) in bit (IntInf.toInt r) (mk q) end;
    1.14    in mk value end;
    1.15  
    1.16  in
    1.17  
    1.18  fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] =
    1.19 -      Syntax.const "Numeral.number_of" $ mk_bin num
    1.20 +      Syntax.const @{const_name Numeral.number_of} $ mk_bin num
    1.21    | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    1.22  
    1.23  end;
    1.24 @@ -39,15 +39,15 @@
    1.25  
    1.26  local
    1.27  
    1.28 -fun dest_bit (Const ("Numeral.bit.B0", _)) = 0
    1.29 -  | dest_bit (Const ("Numeral.bit.B1", _)) = 1
    1.30 +fun dest_bit (Const (@{const_syntax Numeral.bit.B0}, _)) = 0
    1.31 +  | dest_bit (Const (@{const_syntax Numeral.bit.B1}, _)) = 1
    1.32    | dest_bit (Const ("bit.B0", _)) = 0
    1.33    | dest_bit (Const ("bit.B1", _)) = 1
    1.34    | dest_bit _ = raise Match;
    1.35  
    1.36 -fun dest_bin (Const ("\\<^const>Numeral.Pls", _)) = []
    1.37 -  | dest_bin (Const ("\\<^const>Numeral.Min", _)) = [~1]
    1.38 -  | dest_bin (Const ("\\<^const>Numeral.Bit", _) $ bs $ b) = dest_bit b :: dest_bin bs
    1.39 +fun dest_bin (Const (@{const_syntax "Numeral.Pls"}, _)) = []
    1.40 +  | dest_bin (Const (@{const_syntax "Numeral.Min"}, _)) = [~1]
    1.41 +  | dest_bin (Const (@{const_syntax "Numeral.Bit"}, _) $ bs $ b) = dest_bit b :: dest_bin bs
    1.42    | dest_bin _ = raise Match;
    1.43  
    1.44  fun leading _ [] = 0
    1.45 @@ -89,6 +89,6 @@
    1.46  
    1.47  val setup =
    1.48    Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
    1.49 -  Theory.add_trfunsT [("\\<^const>Numeral.number_of", numeral_tr')];
    1.50 +  Theory.add_trfunsT [(@{const_syntax Numeral.number_of}, numeral_tr')];
    1.51  
    1.52  end;