use Syntax.is_ascii_identifier;
authorwenzelm
Mon Apr 26 15:01:05 2004 +0200 (2004-04-26)
changeset 146806029e76841fd
parent 14679 6ed90bd68eda
child 14681 16fcef3a3174
use Syntax.is_ascii_identifier;
src/Pure/Thy/latex.ML
src/Pure/Thy/thm_database.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Mon Apr 26 15:00:20 2004 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Mon Apr 26 15:01:05 2004 +0200
     1.3 @@ -100,7 +100,7 @@
     1.4          if invisible_token tok then ""
     1.5          else if T.is_kind T.Command tok then
     1.6            "\\isacommand{" ^ output_syms s ^ "}"
     1.7 -        else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then
     1.8 +        else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then
     1.9            "\\isakeyword{" ^ output_syms s ^ "}"
    1.10          else if T.is_kind T.String tok then output_syms (Library.quote s)
    1.11          else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
     2.1 --- a/src/Pure/Thy/thm_database.ML	Mon Apr 26 15:00:20 2004 +0200
     2.2 +++ b/src/Pure/Thy/thm_database.ML	Mon Apr 26 15:01:05 2004 +0200
     2.3 @@ -18,8 +18,8 @@
     2.4    val qed_thms: thm list ref
     2.5    val ml_store_thm: string * thm -> unit
     2.6    val ml_store_thms: string * thm list -> unit
     2.7 +  val ml_reserved: string list
     2.8    val is_ml_identifier: string -> bool
     2.9 -  val ml_reserved: string list
    2.10  end;
    2.11  
    2.12  structure ThmDatabase: THM_DATABASE =
    2.13 @@ -51,7 +51,7 @@
    2.14    "struct", "structure", "where"];
    2.15  
    2.16  fun is_ml_identifier name =
    2.17 -  Syntax.is_identifier name andalso not (name mem ml_reserved);
    2.18 +  not (name mem_string ml_reserved) andalso Syntax.is_ascii_identifier name;
    2.19  
    2.20  fun warn_ml name =
    2.21    if is_ml_identifier name then false