replaced is_symid by is_sid;
authorwenzelm
Mon, 16 Nov 1998 10:58:18 +0100
changeset 5876 273056b673ec
parent 5875 6aae55ae3473
child 5877 ee214dec5657
replaced is_symid by is_sid;
src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Mon Nov 16 10:46:06 1998 +0100
+++ b/src/Pure/Isar/outer_lex.ML	Mon Nov 16 10:58:18 1998 +0100
@@ -21,7 +21,7 @@
   val name_of: token -> string
   val is_proper: token -> bool
   val val_of: token -> string
-  val is_symid: string -> bool
+  val is_sid: string -> bool
   val scan: Scan.lexicon ->
     Position.T * Symbol.symbol list -> token * (Position.T * Symbol.symbol list)
   val source: bool -> (unit -> Scan.lexicon) -> Position.T -> (Symbol.symbol, 'a) Source.source ->
@@ -121,9 +121,10 @@
 val sym_chars = explode "!#$%&*+-/:<=>?@^_`|~";
 fun is_sym_char s = s mem sym_chars;
 
-fun is_symid s = s <> "" andalso forall is_sym_char (Symbol.explode s);
+val scan_symid = Scan.any1 is_sym_char >> implode;
 
-val scan_symid = Scan.any1 is_sym_char >> implode;
+fun is_symid s = s <> "" andalso forall is_sym_char (Symbol.explode s);
+val is_sid = is_symid orf Syntax.is_identifier;
 
 
 (* scan strings *)