TFL/thms.sml

    val WFREC_COROLLARY = get_thm WF.thy "tfl_wfrec";
    val WF_INDUCTION_THM = get_thm WF.thy "tfl_wf_induct";
    val CUT_DEF = get_thm WF.thy "cut_def";
 
    val SELECT_AX = prove_goal HOL.thy "!P x. P x --> P (Eps P)"
-     (fn _ => [strip_tac 1, rtac selectI 1, assume_tac 1]);
+     (fn _ => [strip_tac 1, rtac someI 1, assume_tac 1]);
 
    fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
 
    val eqT = prove"(x = True) --> x";
    val rev_eq_mp = prove"(x = y) --> y --> x";