remove_thy: warn unknown theory (rather than error);

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