now using correctly-typed constants from HOLogic
authorpaulson
Fri Jul 23 17:30:27 1999 +0200 (1999-07-23)
changeset 70784e64b2bd10ce
parent 7077 60b098bb8b8a
child 7079 eec20608c791
now using correctly-typed constants from HOLogic
src/HOL/Tools/numeral_syntax.ML
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Fri Jul 23 17:29:12 1999 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Fri Jul 23 17:30:27 1999 +0200
     1.3 @@ -19,8 +19,8 @@
     1.4  
     1.5  (* bits *)
     1.6  
     1.7 -fun mk_bit 0 = Syntax.const "False"
     1.8 -  | mk_bit 1 = Syntax.const "True"
     1.9 +fun mk_bit 0 = HOLogic.false_const
    1.10 +  | mk_bit 1 = HOLogic.true_const
    1.11    | mk_bit _ = sys_error "mk_bit";
    1.12  
    1.13  fun dest_bit (Const ("False", _)) = 0
    1.14 @@ -40,10 +40,9 @@
    1.15        | bin_of ~1 = [~1]
    1.16        | bin_of n  = (n mod 2) :: bin_of (n div 2);
    1.17  
    1.18 -    fun term_of []   = Syntax.const "Numeral.bin.Pls"
    1.19 -      | term_of [~1] = Syntax.const "Numeral.bin.Min"
    1.20 -      | term_of (b :: bs) = Syntax.const "Numeral.bin.Bit" $ term_of bs 
    1.21 -                                                           $ mk_bit b;
    1.22 +    fun term_of []   = HOLogic.pls_const
    1.23 +      | term_of [~1] = HOLogic.min_const
    1.24 +      | term_of (b :: bs) = HOLogic.bit_const $ term_of bs $ mk_bit b;
    1.25      in term_of (bin_of n) end;
    1.26  
    1.27  fun bin_of_string str =