use Syntax.is_ascii_identifier;

--- a/src/Pure/Thy/latex.ML	Mon Apr 26 15:00:20 2004 +0200
+++ b/src/Pure/Thy/latex.ML	Mon Apr 26 15:01:05 2004 +0200
@@ -100,7 +100,7 @@
         if invisible_token tok then ""
         else if T.is_kind T.Command tok then
           "\\isacommand{" ^ output_syms s ^ "}"
-        else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then
+        else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then
           "\\isakeyword{" ^ output_syms s ^ "}"
         else if T.is_kind T.String tok then output_syms (Library.quote s)
         else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)

--- a/src/Pure/Thy/thm_database.ML	Mon Apr 26 15:00:20 2004 +0200
+++ b/src/Pure/Thy/thm_database.ML	Mon Apr 26 15:01:05 2004 +0200
@@ -18,8 +18,8 @@
   val qed_thms: thm list ref
   val ml_store_thm: string * thm -> unit
   val ml_store_thms: string * thm list -> unit
+  val ml_reserved: string list
   val is_ml_identifier: string -> bool
-  val ml_reserved: string list
 end;
 
 structure ThmDatabase: THM_DATABASE =
@@ -51,7 +51,7 @@
   "struct", "structure", "where"];
 
 fun is_ml_identifier name =
-  Syntax.is_identifier name andalso not (name mem ml_reserved);
+  not (name mem_string ml_reserved) andalso Syntax.is_ascii_identifier name;
 
 fun warn_ml name =
   if is_ml_identifier name then false