src/Pure/Thy/thm_database.ML
changeset 5346 bc9748ad8491
parent 5155 21177b8a4d7f
child 5744 9e73738f2307
--- a/src/Pure/Thy/thm_database.ML	Wed Aug 19 17:05:00 1998 +0200
+++ b/src/Pure/Thy/thm_database.ML	Thu Aug 20 09:25:59 1998 +0200
@@ -7,6 +7,7 @@
 
 signature THM_DATABASE =
 sig
+  val ml_store_thm: string * thm -> unit
   val store_thm: string * thm -> thm
   val qed_thm: thm option ref
   val bind_thm: string * thm -> unit