# HG changeset patch
# User wenzelm
# Date 940427451 -7200
# Node ID a5ba4f52991a62adbeb92ef3d1954be3370c9d04
# Parent  c77ad0c3c92f728a158715bdabb25e9a467a220e
remove_thy: warn unknown theory (rather than error);

diff -r c77ad0c3c92f -r a5ba4f52991a src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Oct 20 15:23:55 1999 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Oct 20 15:50:51 1999 +0200
@@ -348,7 +348,8 @@
 (* remove_thy *)
 
 fun remove_thy name =
-  if is_finished name then error (loader_msg "cannot remove finished theory" [name])
+  if is_none (lookup_thy name) then warning (loader_msg "nothing known about theory" [name])
+  else if is_finished name then error (loader_msg "cannot remove finished theory" [name])
   else
     let val succs = thy_graph Graph.all_succs [name] in
       writeln (loader_msg "removing" succs);