# HG changeset patch
# User wenzelm
# Date 1215532348 -7200
# Node ID d2bb5d61b392c89cc36cb636259e14ba2f7a731e
# Parent  0600316f3a3aba830b1fe8b42854f6c8b87c8010
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
non-pervasive touch_thy, remove_thy;

diff -r 0600316f3a3a -r d2bb5d61b392 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Jul 08 17:52:26 2008 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Jul 08 17:52:28 2008 +0200
@@ -6,15 +6,8 @@
 file dependencies.
 *)
 
-signature BASIC_THY_INFO =
-sig
-  val touch_thy: string -> unit
-  val remove_thy: string -> unit
-end;
-
 signature THY_INFO =
 sig
-  include BASIC_THY_INFO
   datatype action = Update | Outdate | Remove
   val str_of_action: action -> string
   val add_hook: (action -> string -> unit) -> unit
@@ -29,6 +22,7 @@
   val master_directory: string -> Path.T
   val loaded_files: string -> Path.T list
   val get_parents: string -> string list
+  val touch_thy: string -> unit
   val touch_child_thys: string -> unit
   val provide_file: Path.T -> string -> unit
   val load_file: bool -> Path.T -> unit
@@ -38,6 +32,8 @@
   val use_thys: string list -> unit
   val use_thy: string -> unit
   val time_use_thy: string -> unit
+  val remove_thy: string -> unit
+  val kill_thy: string -> unit
   val thy_ord: theory * theory -> order
   val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
   val end_theory: theory -> theory
@@ -471,7 +467,7 @@
 end;
 
 
-(* remove_thy *)
+(* remove theory *)
 
 fun remove_thy name =
   if is_finished name then error (loader_msg "cannot remove finished theory" [name])
@@ -481,6 +477,8 @@
       CRITICAL (fn () => (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs)))
     end;
 
+val kill_thy = if_known_thy remove_thy;
+
 
 (* update_time *)
 
@@ -581,5 +579,3 @@
 
 end;
 
-structure BasicThyInfo: BASIC_THY_INFO = ThyInfo;
-open BasicThyInfo;