changeset 18678 | dd0c569fa43d |
parent 18358 | 0a733e11021a |
child 18972 | 2905d1805e1e |
--- a/TFL/tfl.ML Fri Jan 13 17:39:41 2006 +0100 +++ b/TFL/tfl.ML Sat Jan 14 17:14:06 2006 +0100 @@ -578,7 +578,7 @@ val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon theory Hilbert_Choice*) thm "Hilbert_Choice.tfl_some" - handle ERROR => error + handle ERROR msg => cat_error msg "defer_recdef requires theory Main or at least Hilbert_Choice as parent" val bar = R.MP (R.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th in {theory = theory, R=R1, SV=SV,