# HG changeset patch
# User nipkow
# Date 861897803 -7200
# Node ID bbf4e3738ef04b1e60d9166b2c9746318603ef39
# Parent  bb2ded320911771e6c0833babe1b7fdf23c60cd6
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.

diff -r bb2ded320911 -r bbf4e3738ef0 src/Pure/Thy/thy_read.ML
--- 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,