Fixed problem with list_loaded_files and update().

Now when doing use_thy, we don't do an update.
Hopefully "following children are out of date"
message will be superfluous because they will be
unlocked already.  Will be re-read as needed.
Added update function.
Fixed up implementation of list_parents.

1 files changed, 2 insertions, 1 deletions

diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML
index 96bbf66e..9cec27a0 100644
--- a/isa/ProofGeneral.ML
+++ b/isa/ProofGeneral.ML
@@ -105,7 +105,8 @@ structure ProofGeneral =
           end
    in
     (writeln "Updating loaded files list...";
-     seq loading_msg thys_list)
+     seq loading_msg thys_list;
+     writeln "Done.")
    end;
 
  (*