src/Pure/Thy/thy_read.ML

                  Warning: If these functions access reference variables inside
                           READTHY, they have to be redefined each time
                           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 =
 sig
   datatype basetype = Thy  of string

             | get_data ((id, ThyMethods {get, ...}) :: ms) data =
                 get_data ms (Symtab.update ((id, get ()), data));
 
           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,
                              thy_time = thy_time, ml_time = ml_time,
                              theory = theory, thms = thms,