clasohm [Thu, 01 Jun 1995 13:25:06 +0200] rev 1141
commented thms_unifying_with out; placed thm_db into signature again;
placed structures ThmDB and Readthy into Pure again;
changed init_thy_reader so that thm_db and loaded_thys are preserved
(necessary e.g. for ZF)