--- 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