get_thydata accesses the second component of the data field. This component
used to be empty until set at the end of loading an ML file. Now the second
component is already set when the thy file has ben read.

--- a/src/Pure/Thy/thy_read.ML	Thu Apr 24 18:00:22 1997 +0200
+++ b/src/Pure/Thy/thy_read.ML	Thu Apr 24 18:03:23 1997 +0200
@@ -44,7 +44,10 @@
                           init_thy_reader is invoked
         data: user defined data; exn is used to allow arbitrary types;
               first element of pairs contains result that get returned after
-              thy file was read, second element after ML file was read
+              thy file was read, second element after ML file was read;
+              if ML files has not been read, second element is identical to
+              first one because get_thydata, which is meant to return the
+              latest data, always accesses the 2nd element
        *)
 
 signature READTHY =
@@ -661,8 +664,8 @@
 
           val new_data = get_data (Symtab.dest methods) Symtab.null;
 
-          val data' = if thy_only then (new_data, snd data)
-                      else (fst data, new_data);
+          val data' = (if thy_only then new_data else fst data, new_data)
+                      (* 2nd component must be up to date *)
       in loaded_thys := Symtab.update
            ((tname, ThyInfo {path = path,
                              children = children, parents = parents,