# HG changeset patch
# User wenzelm
# Date 1082984465 -7200
# Node ID 6029e76841fd4acd780338d6e040ef723dff5228
# Parent  6ed90bd68eda2b24581925b9036bd97c1d2ac077
use Syntax.is_ascii_identifier;

diff -r 6ed90bd68eda -r 6029e76841fd src/Pure/Thy/latex.ML
--- 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)
diff -r 6ed90bd68eda -r 6029e76841fd src/Pure/Thy/thm_database.ML
--- 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