author | paulson |
Fri, 06 Aug 1999 11:07:25 +0200 | |
changeset 7182 | 090723b5024d |
parent 7181 | 0229127668af |
child 7183 | 9099542ee509 |
--- 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*)