# HG changeset patch
# User wenzelm
# Date 911210298 -3600
# Node ID 273056b673ec48ab38c72967e0955663ea9ef448
# Parent  6aae55ae3473c20447081fbed9917cefb22e2cf8
replaced is_symid by is_sid;

diff -r 6aae55ae3473 -r 273056b673ec 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 *)