src/HOL/Tools/numeral_syntax.ML
changeset 20094 99f27df2b6d0
parent 20067 26bac504ef90
child 21763 12a2773e3608
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Tue Jul 11 14:21:04 2006 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Tue Jul 11 14:21:05 2006 +0200
     1.3 @@ -35,36 +35,11 @@
     1.4      else sign ^ implode (replicate zs "0") ^ num
     1.5    end;
     1.6  
     1.7 +
     1.8  (* translation of integer numeral tokens to and from bitstrings *)
     1.9  
    1.10 -(*additional translations of binary and hex numbers to normal numbers*)
    1.11 -local
    1.12 -
    1.13 -(*get A => ord"0" + 10, etc*)
    1.14 -fun remap_hex c =
    1.15 -  let 
    1.16 -    val zero = ord"0"; 
    1.17 -    val a  = ord"a";
    1.18 -    val ca = ord"A";
    1.19 -    val x  = ord c;
    1.20 -  in
    1.21 -    if x >= a then chr (x - a + zero + 10)
    1.22 -    else if x >= ca then chr (x - ca + zero + 10) 
    1.23 -    else c
    1.24 -  end;
    1.25 -
    1.26 -fun str_to_int' ("0" :: "x" :: ds) = read_radixint (16, map remap_hex ds) |> #1
    1.27 -  | str_to_int' ("0" :: "b" :: ds) = read_radixint (2, ds) |> #1
    1.28 -  | str_to_int' ds = implode ds |> IntInf.fromString |> valOf; 
    1.29 -
    1.30 -in
    1.31 -
    1.32 -val str_to_int = str_to_int' o explode;
    1.33 -
    1.34 -end;
    1.35 -
    1.36  fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] =
    1.37 -      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_binum (str_to_int str)))
    1.38 +      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_binum (Syntax.read_xnum str)))
    1.39    | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    1.40  
    1.41  fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =