# HG changeset patch
# User clasohm
# Date 802005906 -7200
# Node ID a94c0ab9a3ede8bc0d48f37d0513920f45eeadb8
# Parent  0a804a71274aa9689c147bf1dbec2e1d50819216
commented thms_unifying_with out; placed thm_db into signature again;
placed structures ThmDB and Readthy into Pure again;
changed init_thy_reader so that thm_db and loaded_thys are preserved
  (necessary e.g. for ZF)

diff -r 0a804a71274a -r a94c0ab9a3ed src/Pure/Thy/ROOT.ML
--- a/src/Pure/Thy/ROOT.ML	Thu Jun 01 12:31:52 1995 +0200
+++ b/src/Pure/Thy/ROOT.ML	Thu Jun 01 13:25:06 1995 +0200
@@ -18,6 +18,9 @@
 use "thy_read.ML";
 
 structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
+structure ThmDB = ThmdbFUN(val ignore = ["Trueprop", "all", "==>", "=="]);
+structure Readthy = ReadthyFUN(structure ThySyn = ThySyn and ThmDB = ThmDB);
+open ThmDB Readthy;
 
 (* hide functors; saves space in PolyML *)
 functor ThyScanFun() = struct end;
@@ -29,4 +32,7 @@
     \ThmdbFUN(val ignore = [\"Trueprop\",\"all\",\"==>\",\"==\"]);",
     "structure Readthy = ReadthyFUN(structure ThySyn = ThySyn \
                                    \and ThmDB = ThmDB);",
+    "Readthy.loaded_thys := !loaded_thys;",
+    "ThmDB.thm_db := !thm_db;",
+    "val first_init_readthy = false;",
     "open Readthy ThmDB;"];
diff -r 0a804a71274a -r a94c0ab9a3ed src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Thu Jun 01 12:31:52 1995 +0200
+++ b/src/Pure/Thy/thm_database.ML	Thu Jun 01 13:25:06 1995 +0200
@@ -6,9 +6,12 @@
 
 signature THMDB =
 sig
+  type thm_db_type
+
+  val thm_db: thm_db_type
   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
+(*val thms_resolving_with: term * Sign.sg -> (string * thm) list*)
 end;
 
 
@@ -16,11 +19,13 @@
                (*ignore: constants that must not be used for theorem indexing*)
 struct
 
+type thm_db_type = (int * ((int * (string * thm)) list) Symtab.table) ref;
+
 (*Symtab which associates a constant with a list of theorems that contain the
   constant (theorems are represented as numbers)*)
-val thm_db =
-      ref (Symtab.make ([] : (string * ((int * (string * thm)) list)) list));
-val thm_num = ref 0;                                 (*number of next theorem*)
+val thm_db = ref (0,
+           (Symtab.make ([] : (string * ((int * (string * thm)) list)) list)));
+                      (*number of next theorem and symtab containing theorems*)
 
 (*list all relevant constants a term contains*)
 fun list_consts t =
@@ -38,20 +43,21 @@
 
       val consts = distinct (flat (map list_consts (prop :: hyps)));
 
-      val tagged_thm = (!thm_num + 1, named_thm);
+      val (num, db) = !thm_db;
+
+      val tagged_thm = (num + 1, named_thm);
 
-      fun update_db [] = ()
-        | update_db (c :: cs) =
-            let val old_thms = Symtab.lookup_multi (!thm_db, c);
-            in thm_db := Symtab.update ((c, tagged_thm :: old_thms), !thm_db);
-               update_db cs
+      fun update_db [] result = result
+        | update_db (c :: cs) result =
+            let val old_thms = Symtab.lookup_multi (result, c);
+            in update_db cs (Symtab.update ((c, tagged_thm :: old_thms),
+                                            result))
             end;
   in if consts = [] then writeln ("Warning: Theorem " ^ name ^
                                   " cannot be stored in ThmDB\n\t because it \
                                   \contains no or only ignored constants.")
                     else ();
-     update_db consts;
-     thm_num := !thm_num+1;
+     thm_db := (num+1, update_db consts db);
      t
   end;
 
@@ -68,7 +74,7 @@
 fun thms_containing constants =
   let fun collect [] _ result = map snd result
         | collect (c :: cs) first result =
-            let val new_thms = Symtab.lookup_multi (!thm_db, c);
+            let val new_thms = Symtab.lookup_multi (snd (!thm_db), c);
             in collect cs false (if first then new_thms
                                           else (result desc_inter new_thms))
             end;
@@ -80,7 +86,7 @@
      else ();
      collect look_for true [] end;
 
-
+(*This will probably be changed or removed:
 (*get all theorems which can be unified with term t*)
 fun thms_unifying_with(t:term, signt:Sign.sg, thms:(string*thm) list) =
   let val maxt = maxidx_of_term t
@@ -103,4 +109,5 @@
 fun thms_resolving_with (t, sg) =
   let val thms = thms_containing (list_consts t);
   in thms_unifying_with (t, sg, thms) end;
+*)
 end;