src/Pure/Syntax/lexicon.ML
changeset 24630 351a308ab58d
parent 24583 d77e4d48e497
child 26007 3760d3ff4cce
--- a/src/Pure/Syntax/lexicon.ML	Tue Sep 18 11:06:22 2007 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Tue Sep 18 16:08:00 2007 +0200
@@ -29,7 +29,7 @@
   val var: indexname -> term
   val read_nat: string -> int option
   val read_int: string -> int option
-  val read_xnum: string -> {radix: int, leading_zeros: int, value: IntInf.int}
+  val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
   val read_idents: string -> string list
   val fixedN: string
   val constN: string
@@ -402,7 +402,7 @@
       | "0" :: "b" :: cs => (1, 2, cs)
       | "-" :: cs => (~1, 10, cs)
       | cs => (1, 10, cs));
-    val value = IntInf.fromInt sign * #1 (Library.read_intinf radix digs);
+    val value = sign * #1 (Library.read_radix_int radix digs);
   in {radix = radix, leading_zeros = leading_zeros digs, value = value} end;
 
 end;