tuned;

--- a/NEWS	Sun Dec 07 16:05:36 1997 +0100
+++ b/NEWS	Sun Dec 07 16:09:55 1997 +0100
@@ -68,7 +68,8 @@
 use isatool fixseq to adapt your ML programs (this works for fully
 qualified references to the Sequence structure only!);
 
-* use_thy no longer requires writable current directory;
+* use_thy no longer requires writable current directory; it always
+reloads .ML *and* .thy file, if either one is out of date;
 
 
 *** Classical Reasoner ***