added is_ascii_identifier;

--- a/src/Pure/Syntax/lexicon.ML	Mon Apr 26 14:58:54 2004 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Mon Apr 26 15:00:20 2004 +0200
@@ -9,6 +9,7 @@
 signature LEXICON0 =
 sig
   val is_identifier: string -> bool
+  val is_ascii_identifier: string -> bool
   val implode_xstr: string list -> string
   val explode_xstr: string -> string list
   val scan_id: string list -> string * string list
@@ -66,7 +67,7 @@
   val tokenize: Scan.lexicon -> bool -> string list -> token list
 end;
 
-structure Lexicon : LEXICON =
+structure Lexicon: LEXICON =
 struct
 
 
@@ -77,6 +78,10 @@
 
 val is_identifier = is_ident o Symbol.explode;
 
+fun is_ascii_identifier s =
+  let val cs = Symbol.explode s
+  in forall Symbol.is_ascii cs andalso is_ident cs end;
+
 fun is_xid s =
   (case Symbol.explode s of
     "_" :: cs => is_ident cs