# HG changeset patch
# User clasohm
# Date 753475820 -3600
# Node ID 0b0055b3ccfedb74f41fac20982b6f022bf033aa
# Parent  bba27d15d76e152ac1a0330a6085df0b900d5f86
added loaded_thys to signature and removed list_/set_loaded

diff -r bba27d15d76e -r 0b0055b3ccfe src/Pure/Thy/read.ML
--- a/src/Pure/Thy/read.ML	Tue Nov 16 14:26:15 1993 +0100
+++ b/src/Pure/Thy/read.ML	Tue Nov 16 19:50:20 1993 +0100
@@ -20,6 +20,7 @@
   datatype basetype = Thy  of string
                     | File of string
 
+  val loaded_thys    : thy_info list ref
   val loadpath       : string list ref
   val delete_tmpfiles: bool ref
 
@@ -29,8 +30,6 @@
   val unlink_thy     : string -> unit
   val base_on        : basetype list -> string -> Thm.theory
   val store_theory   : string -> Thm.theory -> unit
-  val list_loaded    : unit -> thy_info list
-  val set_loaded     : thy_info list -> unit
 end;
 
 
@@ -446,16 +445,5 @@
                       theory = Some thy}]
   in loaded_thys := make_change (!loaded_thys) end;
 
-(*Create a list of all theories loaded by this structure *)
-fun list_loaded () = (!loaded_thys);
-
-(*Change the list of loaded theories *)
-fun set_loaded [] =
-      loaded_thys := [ThyInfo {name = "Pure", path = "", children = [],
-                      thy_info = Some "", ml_info = Some "",
-                      theory = Some Thm.pure_thy}]
-  | set_loaded ts =
-      loaded_thys := ts;
-
 end