export is_ml_identifier;

--- a/src/Pure/Thy/thm_database.ML	Fri Oct 23 16:27:56 1998 +0200
+++ b/src/Pure/Thy/thm_database.ML	Fri Oct 23 16:44:50 1998 +0200
@@ -8,6 +8,7 @@
 signature THM_DATABASE =
 sig
   val ml_store_thm: string * thm -> unit
+  val is_ml_identifier: string -> bool
   val store_thm: string * thm -> thm
   val qed_thm: thm option ref
   val bind_thm: string * thm -> unit