src/Pure/Thy/ROOT.ML

--- a/src/Pure/Thy/ROOT.ML	Sun May 28 17:18:06 1995 +0200
+++ b/src/Pure/Thy/ROOT.ML	Mon May 29 13:55:06 1995 +0200
@@ -13,22 +13,21 @@
 structure ThyParse = ThyParseFun(structure Symtab = Symtab
   and ThyScan = ThyScan);
 
-(* hide functors; saves space in PolyML *)
-functor ThyScanFun() = struct end;
-functor ThyParseFun() = struct end;
-
 use "thy_syn.ML";
+use "thm_database.ML";
 use "thy_read.ML";
 
 structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
-structure Readthy = ReadthyFUN(structure ThySyn = ThySyn);
-open Readthy;
 
-(* Do not hide ThySynFun and ReadthyFUN; they are still used *)
+(* hide functors; saves space in PolyML *)
+functor ThyScanFun() = struct end;
+functor ThyParseFun() = struct end;
+functor ThySynFun() = struct end;
 
 fun init_thy_reader () =
   use_string
-   ["structure Readthy = ReadthyFUN(structure ThySyn = ThySyn);",
-    "Readthy.loaded_thys := ! loaded_thys;",
-    "open Readthy;"];
-
+   ["structure ThmDB = \
+    \ThmdbFUN(val ignore = [\"Trueprop\",\"All\",\"==>\",\"==\"]);",
+    "structure Readthy = ReadthyFUN(structure ThySyn = ThySyn \
+                                   \and ThmDB = ThmDB);",
+    "open Readthy ThmDB;"];