# HG changeset patch
# User wenzelm
# Date 979601939 -3600
# Node ID 1044648b3f84d97cca4bbae01ad07323112f14a2
# Parent  df4a70b6ad7b41469625d0acaead8d9d64a998c6
use Syntax.read_xnum;

diff -r df4a70b6ad7b -r 1044648b3f84 src/ZF/Tools/numeral_syntax.ML
--- a/src/ZF/Tools/numeral_syntax.ML	Tue Jan 16 00:38:25 2001 +0100
+++ b/src/ZF/Tools/numeral_syntax.ML	Tue Jan 16 00:38:59 2001 +0100
@@ -18,8 +18,6 @@
 structure NumeralSyntax: NUMERAL_SYNTAX =
 struct
 
-open Syntax;
-
 (* Bits *)
 
 val zero = Const("0", iT);
@@ -40,16 +38,6 @@
   | prefix_len pred (x :: xs) =
       if pred x then 1 + prefix_len pred xs else 0;
 
-fun scan_int str =
-  let val (sign, digs) =
-       (case Symbol.explode str of
-	 "#" :: "-" :: cs => (~1, cs)
-       | "#" :: cs => (1, cs)
-       | _ => raise ERROR);
-
-  in  sign * (#1 (read_int digs))  end;
-
-
 val pls_const = Const ("Bin.bin.Pls", iT)
 and min_const = Const ("Bin.bin.Min", iT)
 and bit_const = Const ("Bin.bin.Bit", [iT, iT] ---> iT);
@@ -102,11 +90,10 @@
 (* translation of integer constant tokens to and from binary *)
 
 fun int_tr (*"_Int"*) [t as Free (str, _)] =
-      (const "integ_of" $
-	(mk_bin (scan_int str) handle ERROR => raise TERM ("int_tr", [t])))
+      Syntax.const "integ_of" $ mk_bin (Syntax.read_xnum str)
   | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
 
-fun int_tr' _ _ (*"integ_of"*) [t] = const "_Int" $ free (show_int t)
+fun int_tr' _ _ (*"integ_of"*) [t] = Syntax.const "_Int" $ Syntax.free (show_int t)
   | int_tr' (_:bool) (_:typ)     _ = raise Match;