src/HOL/Tools/numeral_syntax.ML
changeset 10693 9e4a0e84d0d6
parent 9314 fd8b0f219879
child 10891 890b117f6189
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Mon Dec 18 14:57:58 2000 +0100
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Mon Dec 18 14:59:05 2000 +0100
     1.3 @@ -10,7 +10,6 @@
     1.4  signature NUMERAL_SYNTAX =
     1.5  sig
     1.6    val dest_bin : term -> int
     1.7 -  val mk_bin   : int -> term
     1.8    val setup    : (theory -> theory) list
     1.9  end;
    1.10  
    1.11 @@ -20,10 +19,6 @@
    1.12  
    1.13  (* bits *)
    1.14  
    1.15 -fun mk_bit 0 = HOLogic.false_const
    1.16 -  | mk_bit 1 = HOLogic.true_const
    1.17 -  | mk_bit _ = sys_error "mk_bit";
    1.18 -
    1.19  fun dest_bit (Const ("False", _)) = 0
    1.20    | dest_bit (Const ("True", _)) = 1
    1.21    | dest_bit _ = raise Match;
    1.22 @@ -35,17 +30,6 @@
    1.23    | prefix_len pred (x :: xs) =
    1.24        if pred x then 1 + prefix_len pred xs else 0;
    1.25  
    1.26 -fun mk_bin n =
    1.27 -  let
    1.28 -    fun bin_of 0  = []
    1.29 -      | bin_of ~1 = [~1]
    1.30 -      | bin_of n  = (n mod 2) :: bin_of (n div 2);
    1.31 -
    1.32 -    fun term_of []   = HOLogic.pls_const
    1.33 -      | term_of [~1] = HOLogic.min_const
    1.34 -      | term_of (b :: bs) = HOLogic.bit_const $ term_of bs $ mk_bit b;
    1.35 -    in term_of (bin_of n) end;
    1.36 -
    1.37  (*we consider all "spellings"; Min is likely to be declared elsewhere*)
    1.38  fun bin_of (Const ("Pls", _)) = []
    1.39    | bin_of (Const ("bin.Pls", _)) = []
    1.40 @@ -74,7 +58,7 @@
    1.41  (* translation of integer numeral tokens to and from bitstrings *)
    1.42  
    1.43  fun numeral_tr (*"_Numeral"*) [t as Free (str, _)] =
    1.44 -      (Syntax.const "Numeral.number_of" $ mk_bin (Syntax.read_xnum str))
    1.45 +      (Syntax.const "Numeral.number_of" $ HOLogic.mk_bin (Syntax.read_xnum str))
    1.46    | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    1.47  
    1.48  fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =