added read_nat;

--- a/src/Pure/Syntax/lexicon.ML	Fri Nov 13 13:42:23 1998 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Sat Nov 14 13:23:49 1998 +0100
@@ -28,6 +28,7 @@
   val dest_binding: string -> string
   val skolem: string -> string
   val dest_skolem: string -> string
+  val read_nat: string -> int option
 end;
 
 signature LEXICON =
@@ -334,4 +335,12 @@
 val dest_skolem = unsuffix "__";
 
 
+(* read_nat *)
+
+fun read_nat str =
+  (case Scan.finite Symbol.stopper (Scan.option scan_digits1) (Symbol.explode str) of
+    (Some cs, []) => Some (#1 (Term.read_int cs))
+  | _ => None);
+
+
 end;