# HG changeset patch
# User wenzelm
# Date 1152620465 -7200
# Node ID 99f27df2b6d0bbb30783207b425efa77fb13311f
# Parent  164a42b7385fef0396d87ccc7918b0fbe26d0491
removed str_to_int in favour of general Syntax.read_xnum;

diff -r 164a42b7385f -r 99f27df2b6d0 src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Tue Jul 11 14:21:04 2006 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML	Tue Jul 11 14:21:05 2006 +0200
@@ -35,36 +35,11 @@
     else sign ^ implode (replicate zs "0") ^ num
   end;
 
+
 (* translation of integer numeral tokens to and from bitstrings *)
 
-(*additional translations of binary and hex numbers to normal numbers*)
-local
-
-(*get A => ord"0" + 10, etc*)
-fun remap_hex c =
-  let 
-    val zero = ord"0"; 
-    val a  = ord"a";
-    val ca = ord"A";
-    val x  = ord c;
-  in
-    if x >= a then chr (x - a + zero + 10)
-    else if x >= ca then chr (x - ca + zero + 10) 
-    else c
-  end;
-
-fun str_to_int' ("0" :: "x" :: ds) = read_radixint (16, map remap_hex ds) |> #1
-  | str_to_int' ("0" :: "b" :: ds) = read_radixint (2, ds) |> #1
-  | str_to_int' ds = implode ds |> IntInf.fromString |> valOf; 
-
-in
-
-val str_to_int = str_to_int' o explode;
-
-end;
-
 fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] =
-      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_binum (str_to_int str)))
+      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_binum (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) =