moved is_ident to General/symbol.ML;

--- a/src/Pure/Syntax/lexicon.ML	Tue May 31 11:53:40 2005 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Tue May 31 11:53:41 2005 +0200
@@ -72,23 +72,20 @@
 
 (** is_identifier etc. **)
 
-fun is_ident [] = false
-  | is_ident (c :: cs) = Symbol.is_letter c andalso forall Symbol.is_letdig cs;
-
-val is_identifier = is_ident o Symbol.explode;
+val is_identifier = Symbol.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;
+  in forall Symbol.is_ascii cs andalso Symbol.is_ident cs end;
 
 fun is_xid s =
   (case Symbol.explode s of
-    "_" :: cs => is_ident cs
-  | cs => is_ident cs);
+    "_" :: cs => Symbol.is_ident cs
+  | cs => Symbol.is_ident cs);
 
 fun is_tid s =
   (case Symbol.explode s of
-    "'" :: cs => is_ident cs
+    "'" :: cs => Symbol.is_ident cs
   | _ => false);