# HG changeset patch
# User wenzelm
# Date 911046229 -3600
# Node ID ed11c98908527e5a32cfe5bf16372efbd7e7e048
# Parent  87595fc9508918dc79347061f6ab2078bb044b0d
added read_nat;

diff -r 87595fc95089 -r ed11c9890852 src/Pure/Syntax/lexicon.ML
--- 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;