diff -r 01265301db7f -r dd0c569fa43d TFL/tfl.ML
--- 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,