# HG changeset patch
# User wenzelm
# Date 870869523 -7200
# Node ID 3d0d5f2a2e334f5902e3be13a3db06cce1a9bf6f
# Parent  d91708377b6ac3f97c878da653fff72e54e8c240
tuned names;

diff -r d91708377b6a -r 3d0d5f2a2e33 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Wed Aug 06 14:11:08 1997 +0200
+++ b/src/Pure/Thy/thm_database.ML	Wed Aug 06 14:12:03 1997 +0200
@@ -4,7 +4,7 @@
     Copyright   1995 TU Muenchen
 *)
 
-datatype thm_db_type =
+datatype thm_db =
   ThmDB of {count: int,
             thy_idx: (Sign.sg * (string list * int list)) list,
             const_idx: ((int * (string * thm)) list) Symtab.table};
@@ -14,9 +14,9 @@
       const_idx: named theorems tagged by numbers and
                  indexed by the constants they contain*)
 
-signature THMDB =
+signature THM_DATABASE =
   sig
-  val thm_db: thm_db_type ref
+  val thm_db: thm_db ref
   val store_thm_db: string * thm -> thm
   val delete_thm_db: theory -> unit
   val thms_containing: string list -> (string * thm) list
@@ -39,7 +39,7 @@
   val print_theory   : theory -> unit
   end;
 
-structure ThmDB: THMDB =
+structure ThmDatabase: THM_DATABASE =
 struct
 
 open ThyInfo BrowserInfo;