now catches exn THEORY and prints an error message

--- a/src/Pure/Thy/thm_database.ML	Fri Aug 06 11:06:16 1999 +0200
+++ b/src/Pure/Thy/thm_database.ML	Fri Aug 06 11:07:25 1999 +0200
@@ -77,7 +77,8 @@
     val sign = sign_of_thm (topthm ());
     val consts = map (Sign.intern_const sign) raw_consts;
     val thy = ThyInfo.theory_of_sign sign;
-  in PureThy.thms_containing thy consts end;
+  in PureThy.thms_containing thy consts end
+  handle THEORY (msg,_) => error msg;
 
 
 (*top_const: main constant, ignoring Trueprop*)