# HG changeset patch
# User wenzelm
# Date 878056452 -3600
# Node ID 4e2994bae718f5e38351a3af339537a18520fd73
# Parent  f88775cc8d178e6b553032cee2efcbd3c38d9b32
always reload .ML *and* .thy file;

diff -r f88775cc8d17 -r 4e2994bae718 src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Tue Oct 28 17:32:38 1997 +0100
+++ b/src/Pure/Thy/thy_read.ML	Tue Oct 28 17:34:12 1997 +0100
@@ -278,27 +278,14 @@
   in if thy_uptodate andalso ml_uptodate then ()
      else
       (if thy_file = "" then ()
-       else if thy_uptodate then put_thydata true tname
        else
          (writeln ("Reading \"" ^ name ^ ".thy\"");
 
           init_thyinfo ();
-          delete_thms tname;
           read_thy tname thy_file;
           SymbolInput.use (out_name tname);
           save_data true;
 
-          (*Store axioms of theory
-            (but only if it's not a copy of an older theory)*)
-          let val parents = parents_of_name tname;
-              val this_thy = theory_of tname;
-              val axioms =
-                if length parents = 1
-                   andalso Sign.eq_sg (sign_of (theory_of (hd parents)),
-                                       sign_of this_thy) then []
-                else axioms_of this_thy;
-          in map store_thm_db axioms end;
-
           if not (!delete_tmpfiles) then ()
           else OS.FileSys.remove (out_name tname);