1.1 --- a/src/Pure/Thy/thy_info.ML	Wed Oct 20 15:23:55 1999 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Oct 20 15:50:51 1999 +0200
     1.3 @@ -348,7 +348,8 @@
     1.4  (* remove_thy *)
     1.5  
     1.6  fun remove_thy name =
     1.7 -  if is_finished name then error (loader_msg "cannot remove finished theory" [name])
     1.8 +  if is_none (lookup_thy name) then warning (loader_msg "nothing known about theory" [name])
     1.9 +  else if is_finished name then error (loader_msg "cannot remove finished theory" [name])
    1.10    else
    1.11      let val succs = thy_graph Graph.all_succs [name] in
    1.12        writeln (loader_msg "removing" succs);