defer_recdef (lazyR_def) now looks for theorem Hilbert_Choice.tfl_some
dynamically, so recdef no longer needs to import Hilbert_Choice.

--- 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)),

--- a/TFL/thms.ML	Wed Jul 25 17:58:26 2001 +0200
+++ b/TFL/thms.ML	Wed Jul 25 18:21:01 2001 +0200
@@ -9,7 +9,6 @@
   val WFREC_COROLLARY = thm "tfl_wfrec";
   val WF_INDUCTION_THM = thm "tfl_wf_induct";
   val CUT_DEF = thm "cut_def";
-  val SELECT_AX = thm "tfl_some";
   val eqT = thm "tfl_eq_True";
   val rev_eq_mp = thm "tfl_rev_eq_mp";
   val simp_thm = thm "tfl_simp_thm";