changeset 7182 | 090723b5024d |
parent 6327 | c6abb5884fed |
child 7410 | 7369a35fb3c2 |
--- 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*)