# HG changeset patch
# User wenzelm
# Date 1026986948 -7200
# Node ID 553e7b62680f6351d68271ac139f723081baa954
# Parent  c48c634605f101c6d4f9be93249879f9e1d30aa4
fixed inform_file_retracted: remove_thy;

diff -r c48c634605f1 -r 553e7b62680f src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Thu Jul 18 12:08:45 2002 +0200
+++ b/src/Pure/proof_general.ML	Thu Jul 18 12:09:08 2002 +0200
@@ -11,8 +11,8 @@
   val setup: (theory -> theory) list
   val update_thy_only: string -> unit
   val try_update_thy_only: string -> unit
+  val inform_file_retracted: string -> unit
   val inform_file_processed: string -> unit
-  val inform_file_retracted: string -> unit
   val thms_containing: string list -> unit
   val help: unit -> unit
   val show_context: unit -> theory
@@ -202,14 +202,12 @@
 
 (* get informed about files *)
 
-val touch_child_thys = ThyInfo.if_known_thy ThyInfo.touch_child_thys;
-
-val inform_file_processed = touch_child_thys o thy_name;
-val inform_file_retracted = touch_child_thys o thy_name;
+val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
+val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
 
 fun proper_inform_file_processed file state =
   let val name = thy_name file in
-    touch_child_thys name;
+    ThyInfo.if_known_thy ThyInfo.touch_child_thys name;
     if not (Toplevel.is_toplevel state) then
       warning ("Not at toplevel -- cannot register theory " ^ quote name)
     else Library.transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>