src/Pure/Syntax/lexicon.ML
changeset 14835 695ee8ad0bb6
parent 14783 e7f7ed4c06f2
child 14981 e73f8140af78
--- 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) *)