--- a/src/HOL/Filter.thy Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Filter.thy Sun Dec 13 21:56:15 2015 +0100
@@ -233,24 +233,23 @@
frequently_imp_iff
ML \<open>
- fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
- let
- val mp_thms = facts RL @{thms eventually_rev_mp}
- val raw_elim_thm =
- (@{thm allI} RS @{thm always_eventually})
- |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
- |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
- val cases_prop =
- Thm.prop_of
- (Rule_Cases.internalize_params (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal)))
- val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
- in
- CASES cases (resolve_tac ctxt [raw_elim_thm] i)
- end)
+ fun eventually_elim_tac facts =
+ CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
+ let
+ val mp_thms = facts RL @{thms eventually_rev_mp}
+ val raw_elim_thm =
+ (@{thm allI} RS @{thm always_eventually})
+ |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
+ |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
+ val cases_prop =
+ Thm.prop_of
+ (Rule_Cases.internalize_params (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal)))
+ val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
+ in CONTEXT_CASES cases (resolve_tac ctxt [raw_elim_thm] i) (ctxt, st) end)
\<close>
method_setup eventually_elim = \<open>
- Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
+ Scan.succeed (fn _ => CONTEXT_METHOD (fn facts => eventually_elim_tac facts 1))
\<close> "elimination of eventually quantifiers"
subsubsection \<open>Finer-than relation\<close>