# HG changeset patch
# User wenzelm
# Date 909153890 -7200
# Node ID 9e73738f2307586342c9ecdf3f3679a6abf5a928
# Parent  f2cf404a9579b841d9991dee0aeb795cdcb28cfb
export is_ml_identifier;

diff -r f2cf404a9579 -r 9e73738f2307 src/Pure/Thy/thm_database.ML
--- 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