diff -r fa09705a5890 -r 3d408455d69f src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Fri Sep 01 13:32:13 1995 +0200
+++ b/src/Pure/Thy/thy_read.ML	Fri Sep 01 13:51:49 1995 +0200
@@ -358,20 +358,10 @@
             Some (gen_rems same_thm (#simps(rep_ss (!simpset)), !old_simps)))
          );
 
-       (*Store theory again because it could have been redefined*)
-       use_string
-         ["val _ = (store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ "); " ^
-
-       (*Store new axioms in theorem database; ignore theories which are just
-         copies of existing ones*)
-       let val parents = get_parents tname;
-           val fst_thy = get_theory (hd parents);
-           val this_thy = get_theory tname;
-       in if length parents = 1
-             andalso Sign.eq_sg (sign_of fst_thy, sign_of this_thy) then ""
-          else
-            "map store_thm_db (axioms_of " ^ tname ^ ".thy));"
-       end];
+         use_string
+           ["val _ = (store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");\
+            \map store_thm_db (axioms_of " ^ tname ^ ".thy));"];
+                    (*Store theory again because it could have been redefined*)
 
        (*Now set the correct info*)
        set_info (Some (file_info thy_file)) (Some (file_info ml_file)) tname;