src/Pure/Thy/thm_database.ML
changeset 1137 1a768988f8e3
parent 1136 3910c96551d1
child 1141 a94c0ab9a3ed
--- a/src/Pure/Thy/thm_database.ML	Tue May 30 11:28:13 1995 +0200
+++ b/src/Pure/Thy/thm_database.ML	Tue May 30 11:57:27 1995 +0200
@@ -6,8 +6,6 @@
 
 signature THMDB =
 sig
-  val thm_db: (int * (string * thm)) list Symtab.table ref
-  val thm_num: int ref
   val store_thm_db: string * thm -> thm
   val thms_containing: string list -> (string * thm) list
   val thms_resolving_with: term * Sign.sg -> (string * thm) list