diff -r 7514e5e21cb8 -r e07927b980ec TFL/tfl.ML
--- a/TFL/tfl.ML	Wed Jul 25 17:58:26 2001 +0200
+++ b/TFL/tfl.ML	Wed Jul 25 18:21:01 2001 +0200
@@ -571,8 +571,12 @@
                 RS meta_eq_to_obj_eq
      val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0
      val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop)
-     val bar = R.MP (R.ISPECL[tych R'abs, tych R1] Thms.SELECT_AX)
-                    body_th
+     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
+    "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,
      rules = U.rev_itlist (U.C R.MP) (R.CONJUNCTS bar) def',
      full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),