# HG changeset patch # User paulson # Date 996078061 -7200 # Node ID e07927b980ec18f949d44e007939f4c88c941b5d # Parent 7514e5e21cb82170c91e4a9cfd2f64bd8623a346 defer_recdef (lazyR_def) now looks for theorem Hilbert_Choice.tfl_some dynamically, so recdef no longer needs to import Hilbert_Choice. 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)), diff -r 7514e5e21cb8 -r e07927b980ec TFL/thms.ML --- 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";