diff -r e47744683560 -r 695ee8ad0bb6 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sat May 29 15:06:19 2004 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Sat May 29 15:06:42 2004 +0200
@@ -360,7 +360,7 @@
 (* read_nat *)
 
 fun read_nat str =
-  apsome (#1 o Term.read_int) (Scan.read Symbol.stopper scan_digits1 (Symbol.explode str));
+  apsome (#1 o Library.read_int) (Scan.read Symbol.stopper scan_digits1 (Symbol.explode str));
 
 
 (* read_xnum *)
@@ -373,7 +373,7 @@
       | "#" :: cs => (1, cs)
       | "-" :: cs => (~1, cs)
       | cs => (1, cs));
-  in sign * #1 (Term.read_int digs) end;
+  in sign * #1 (Library.read_int digs) end;
 
 
 (* read_ident(s) *)