moved call of store_theory to end of use t.thy; use t.ML;
use_thy now needs the exact theory name (capital/lower letters);
improved handling of incompletly read theories;
added function unlink_thy, removed function relations;
added reference variable delete_tmpfile;
removed some bugs