src/Pure/Thy/thy_info.ML
changeset 5211 c02b0c727780
parent 5209 a69fe5a61b6c
child 6211 43d0efafa025
     1.1 --- a/src/Pure/Thy/thy_info.ML	Tue Jul 28 17:05:34 1998 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Jul 29 15:38:08 1998 +0200
     1.3 @@ -36,6 +36,7 @@
     1.4  signature THY_INFO =
     1.5  sig
     1.6    include BASIC_THY_INFO
     1.7 +  val mk_info: string * string list * string list * theory -> string * thy_info
     1.8    val loaded_thys: thy_info Symtab.table ref
     1.9    val get_thyinfo: string -> thy_info option
    1.10    val store_theory: theory -> unit
    1.11 @@ -58,11 +59,7 @@
    1.12      thy_time = Some "", ml_time = Some "", theory = Some theory}: thy_info);
    1.13  
    1.14  (*preloaded theories*)
    1.15 -val loaded_thys =
    1.16 -  ref (Symtab.make (map mk_info
    1.17 -    [("ProtoPure", ["Pure", "CPure"], [], ProtoPure.thy),
    1.18 -     ("Pure", [], ["ProtoPure"], Pure.thy),
    1.19 -     ("CPure", [], ["ProtoPure"], CPure.thy)]));
    1.20 +val loaded_thys = ref (Symtab.empty: thy_info Symtab.table);
    1.21  
    1.22  
    1.23  (* retrieve info *)