# HG changeset patch
# User wenzelm
# Date 1117533221 -7200
# Node ID c33fe18456fa9ab029f3c8c2b70296649a2331b2
# Parent  d8cac577493c3d739c1bacbb4570b6c34b4fc996
moved is_ident to General/symbol.ML;

diff -r d8cac577493c -r c33fe18456fa src/Pure/Syntax/lexicon.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);