# HG changeset patch
# User wenzelm
# Date 1158858363 -7200
# Node ID 21e096f30c5d52116352acc7506a0d9a39f076c4
# Parent  cb19d18aef01f6062790faf0452e27bad0905fd5
added is_ml_reserved;

diff -r cb19d18aef01 -r 21e096f30c5d src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Thu Sep 21 19:05:56 2006 +0200
+++ b/src/Pure/Thy/thm_database.ML	Thu Sep 21 19:06:03 2006 +0200
@@ -20,6 +20,7 @@
   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;
 
@@ -51,8 +52,10 @@
   "eqtype", "functor", "include", "sharing", "sig", "signature",
   "struct", "structure", "where"];
 
+val is_ml_reserved = member (op =) ml_reserved;
+
 fun is_ml_identifier name =
-  not (name mem_string ml_reserved) andalso Syntax.is_ascii_identifier name;
+  not (is_ml_reserved name) andalso Syntax.is_ascii_identifier name;
 
 fun warn_ml name =
   if is_ml_identifier name then false