diff -r 98d35a7368bd -r fb579401dc26 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Mon Nov 26 21:10:42 2012 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Mon Nov 26 21:46:04 2012 +0100
@@ -12,9 +12,6 @@
     val free: string -> term
     val var: indexname -> term
   end
-  val is_identifier: string -> bool
-  val is_xid: string -> bool
-  val is_tid: string -> bool
   val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
@@ -25,6 +22,7 @@
   val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+  val is_tid: string -> bool
   datatype token_kind =
     Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
     NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF
@@ -90,32 +88,13 @@
 
 
 
-(** is_identifier etc. **)
-
-val is_identifier = Symbol.is_ident o Symbol.explode;
-
-fun is_xid s =
-  (case Symbol.explode s of
-    "_" :: cs => Symbol.is_ident cs
-  | cs => Symbol.is_ident cs);
-
-fun is_tid s =
-  (case Symbol.explode s of
-    "'" :: cs => Symbol.is_ident cs
-  | _ => false);
-
-
-
 (** basic scanners **)
 
 open Basic_Symbol_Pos;
 
 fun !!! msg = Symbol_Pos.!!! (fn () => "Inner lexical error: " ^ msg);
 
-val scan_id =
-  Scan.one (Symbol.is_letter o Symbol_Pos.symbol) :::
-  Scan.many (Symbol.is_letdig o Symbol_Pos.symbol);
-
+val scan_id = Symbol_Pos.scan_ident;
 val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
 val scan_tid = $$$ "'" @@@ scan_id;
 
@@ -130,6 +109,11 @@
 val scan_var = $$$ "?" @@@ scan_id_nat;
 val scan_tvar = $$$ "?" @@@ $$$ "'" @@@ scan_id_nat;
 
+fun is_tid s =
+  (case try (unprefix "'") s of
+    SOME s' => Symbol_Pos.is_identifier s'
+  | NONE => false);
+
 
 
 (** datatype token **)
@@ -315,7 +299,8 @@
           if Symbol.is_digit c then chop_idx cs (c :: ds)
           else idxname (c :: cs) ds;
 
-    val scan = (scan_id >> map Symbol_Pos.symbol) --
+    val scan =
+      (scan_id >> map Symbol_Pos.symbol) --
       Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
   in
     scan >>