diff -r 54aaa779b6b4 -r c02b0c727780 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Jul 28 17:05:34 1998 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Jul 29 15:38:08 1998 +0200
@@ -36,6 +36,7 @@
 signature THY_INFO =
 sig
   include BASIC_THY_INFO
+  val mk_info: string * string list * string list * theory -> string * thy_info
   val loaded_thys: thy_info Symtab.table ref
   val get_thyinfo: string -> thy_info option
   val store_theory: theory -> unit
@@ -58,11 +59,7 @@
     thy_time = Some "", ml_time = Some "", theory = Some theory}: thy_info);
 
 (*preloaded theories*)
-val loaded_thys =
-  ref (Symtab.make (map mk_info
-    [("ProtoPure", ["Pure", "CPure"], [], ProtoPure.thy),
-     ("Pure", [], ["ProtoPure"], Pure.thy),
-     ("CPure", [], ["ProtoPure"], CPure.thy)]));
+val loaded_thys = ref (Symtab.empty: thy_info Symtab.table);
 
 
 (* retrieve info *)