# HG changeset patch # User wenzelm # Date 1428522128 -7200 # Node ID 046399298519f8a0fa6449a1fd04f2fe7bdf9344 # Parent da10875adf8e7cd05513cf34008240aea6c4aa4c more standard access to goal state; diff -r da10875adf8e -r 046399298519 src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Wed Apr 08 21:24:27 2015 +0200 +++ b/src/HOL/Topological_Spaces.thy Wed Apr 08 21:42:08 2015 +0200 @@ -443,22 +443,22 @@ qed ML {* - fun eventually_elim_tac ctxt thms st = SUBGOAL_CASES (fn _ => + fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) => let - val mp_thms = thms RL [@{thm eventually_rev_mp}] + 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) thms - val cases_prop = Thm.prop_of (raw_elim_thm RS st) + |> fold (fn _ => fn thm => @{thm impI} RS thm) facts + val cases_prop = Thm.prop_of (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal)) val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])] in - CASES cases (rtac raw_elim_thm 1) - end) 1 st + CASES cases (rtac raw_elim_thm i) + end) *} method_setup eventually_elim = {* - Scan.succeed (fn ctxt => METHOD_CASES (eventually_elim_tac ctxt)) + Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt)) *} "elimination of eventually quantifiers"