src/Pure/General/symbol.ML
changeset 13559 51c3ac47d127
parent 12904 c208d71702d1
child 13730 09aeb7346d3f
--- a/src/Pure/General/symbol.ML	Tue Sep 03 18:49:30 2002 +0200
+++ b/src/Pure/General/symbol.ML	Thu Sep 05 14:03:03 2002 +0200
@@ -26,6 +26,7 @@
   val is_quasi_letter: symbol -> bool
   val is_letdig: symbol -> bool
   val is_blank: symbol -> bool
+  val is_identifier: symbol -> bool
   val is_symbolic: symbol -> bool
   val is_printable: symbol -> bool
   val length: symbol list -> int
@@ -111,6 +112,10 @@
   size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse
   is_symbolic s;
 
+fun is_identifier s =
+  case (explode s) of
+      [] => false
+    | c::cs => is_letter c andalso forall is_letdig cs;
 
 fun sym_length ss = foldl (fn (n, s) =>
   (if not (is_printable s) then 0 else