# HG changeset patch
# User wenzelm
# Date 963522698 -7200
# Node ID fd8b0f2198796983146d8e9cc16736fa3245950e
# Parent  b5a29408dc39ad60d1904a8b5a30d88307e084b7
use Syntax.read_xnum;

diff -r b5a29408dc39 -r fd8b0f219879 src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Thu Jul 13 23:11:14 2000 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML	Thu Jul 13 23:11:38 2000 +0200
@@ -46,15 +46,6 @@
       | term_of (b :: bs) = HOLogic.bit_const $ term_of bs $ mk_bit b;
     in term_of (bin_of n) end;
 
-fun bin_of_string str =
-  let
-    val (sign, digs) =
-      (case Symbol.explode str of
-        "#" :: "-" :: cs => (~1, cs)
-      | "#" :: cs => (1, cs)
-      | _ => raise ERROR);
-    in mk_bin (sign * (#1 (Term.read_int digs))) end;
-
 (*we consider all "spellings"; Min is likely to be declared elsewhere*)
 fun bin_of (Const ("Pls", _)) = []
   | bin_of (Const ("bin.Pls", _)) = []
@@ -83,8 +74,7 @@
 (* translation of integer numeral tokens to and from bitstrings *)
 
 fun numeral_tr (*"_Numeral"*) [t as Free (str, _)] =
-      (Syntax.const "Numeral.number_of" $
-        (bin_of_string str handle ERROR => raise TERM ("numeral_tr", [t])))
+      (Syntax.const "Numeral.number_of" $ mk_bin (Syntax.read_xnum str))
   | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
 
 fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =