use Syntax.read_xnum;
authorwenzelm
Thu Jul 13 23:11:38 2000 +0200 (2000-07-13)
changeset 9314fd8b0f219879
parent 9313 b5a29408dc39
child 9315 f793f05024f6
use Syntax.read_xnum;
src/HOL/Tools/numeral_syntax.ML
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Thu Jul 13 23:11:14 2000 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Thu Jul 13 23:11:38 2000 +0200
     1.3 @@ -46,15 +46,6 @@
     1.4        | term_of (b :: bs) = HOLogic.bit_const $ term_of bs $ mk_bit b;
     1.5      in term_of (bin_of n) end;
     1.6  
     1.7 -fun bin_of_string str =
     1.8 -  let
     1.9 -    val (sign, digs) =
    1.10 -      (case Symbol.explode str of
    1.11 -        "#" :: "-" :: cs => (~1, cs)
    1.12 -      | "#" :: cs => (1, cs)
    1.13 -      | _ => raise ERROR);
    1.14 -    in mk_bin (sign * (#1 (Term.read_int digs))) end;
    1.15 -
    1.16  (*we consider all "spellings"; Min is likely to be declared elsewhere*)
    1.17  fun bin_of (Const ("Pls", _)) = []
    1.18    | bin_of (Const ("bin.Pls", _)) = []
    1.19 @@ -83,8 +74,7 @@
    1.20  (* translation of integer numeral tokens to and from bitstrings *)
    1.21  
    1.22  fun numeral_tr (*"_Numeral"*) [t as Free (str, _)] =
    1.23 -      (Syntax.const "Numeral.number_of" $
    1.24 -        (bin_of_string str handle ERROR => raise TERM ("numeral_tr", [t])))
    1.25 +      (Syntax.const "Numeral.number_of" $ mk_bin (Syntax.read_xnum str))
    1.26    | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    1.27  
    1.28  fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =