src/Pure/Syntax/lexicon.ML

     val const: string -> term
     val free: string -> term
     val var: indexname -> term
   end
   val is_identifier: string -> bool
-  val is_ascii_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

 
 (** is_identifier etc. **)
 
 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 Symbol.is_ident cs end;
-
 fun is_xid s =
   (case Symbol.explode s of
     "_" :: cs => Symbol.is_ident cs
   | cs => Symbol.is_ident cs);
 

 
 
 (* markup *)
 
 fun literal_markup s =
-  if is_ascii_identifier s then Markup.literal else Markup.delimiter;
+  if Symbol.is_ascii_identifier s then Markup.literal else Markup.delimiter;
 
 val token_kind_markup =
  fn VarSy   => Markup.var
   | TFreeSy => Markup.tfree
   | TVarSy  => Markup.tvar