# HG changeset patch
# User wenzelm
# Date 1164239539 -3600
# Node ID 7bb5de80917fa71b52e8fd74467e53afa69e792d
# Parent  025ab31286d8219f65aee58aa726716759017038
moved ML identifiers to structure ML_Syntax;

diff -r 025ab31286d8 -r 7bb5de80917f src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Thu Nov 23 00:52:15 2006 +0100
+++ b/src/Pure/Thy/thm_database.ML	Thu Nov 23 00:52:19 2006 +0100
@@ -19,9 +19,6 @@
   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_reserved: string -> bool
-  val is_ml_identifier: string -> bool
 end;
 
 structure ThmDatabase: THM_DATABASE =
@@ -44,21 +41,8 @@
 
 val qed_thms: thm list ref = ref [];
 
-val ml_reserved =
- ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else",
-  "end", "exception", "fn", "fun", "handle", "if", "in", "infix",
-  "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse",
-  "raise", "rec", "then", "type", "val", "with", "withtype", "while",
-  "eqtype", "functor", "include", "sharing", "sig", "signature",
-  "struct", "structure", "where"];
-
-val is_ml_reserved = member (op =) ml_reserved;
-
-fun is_ml_identifier name =
-  not (is_ml_reserved name) andalso Syntax.is_ascii_identifier name;
-
 fun warn_ml name =
-  if is_ml_identifier name then false
+  if ML_Syntax.is_identifier name then false
   else if name = "" then true
   else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
 
@@ -89,7 +73,8 @@
       let
         val xname = NameSpace.extern space name;
         fun result prfx bname =
-          if (prfx = "" orelse is_ml_identifier prfx) andalso is_ml_identifier bname andalso
+          if (prfx = "" orelse ML_Syntax.is_identifier prfx) andalso
+              ML_Syntax.is_identifier bname andalso
               NameSpace.intern space xname = name then
             SOME (prfx, (bname, xname, length (the (Symtab.lookup thms name)) = 1))
           else NONE;