# HG changeset patch
# User paulson
# Date 933930445 -7200
# Node ID 090723b5024d902971559ef1e1821b58922b4ec6
# Parent  0229127668afe990736b3c0bb0a42b25f7f56fad
now catches exn THEORY and prints an error message

diff -r 0229127668af -r 090723b5024d src/Pure/Thy/thm_database.ML
--- 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*)