--- a/src/Pure/General/symbol.ML Tue May 31 11:53:28 2005 +0200
+++ b/src/Pure/General/symbol.ML Tue May 31 11:53:29 2005 +0200
@@ -39,6 +39,7 @@
val is_blank: symbol -> bool
val is_quasi_letter: symbol -> bool
val is_letdig: symbol -> bool
+ val is_ident: symbol list -> bool
val beginning: int -> symbol list -> string
val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a
val scan_id: string list -> string * string list
@@ -353,6 +354,9 @@
fun is_quasi_letter s = let val k = kind s in k = Letter orelse k = Quasi end;
fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end;
+fun is_ident [] = false
+ | is_ident (c :: cs) = is_letter c andalso forall is_letdig cs;
+
(** symbol input **)