more standard access to goal state;
authorwenzelm
Wed Apr 08 21:42:08 2015 +0200 (2015-04-08)
changeset 59976046399298519
parent 59975 da10875adf8e
child 59977 ad2d1cd53877
more standard access to goal state;
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Topological_Spaces.thy	Wed Apr 08 21:24:27 2015 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Apr 08 21:42:08 2015 +0200
     1.3 @@ -443,22 +443,22 @@
     1.4  qed
     1.5  
     1.6  ML {*
     1.7 -  fun eventually_elim_tac ctxt thms st = SUBGOAL_CASES (fn _ =>
     1.8 +  fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
     1.9      let
    1.10 -      val mp_thms = thms RL [@{thm eventually_rev_mp}]
    1.11 +      val mp_thms = facts RL @{thms eventually_rev_mp}
    1.12        val raw_elim_thm =
    1.13          (@{thm allI} RS @{thm always_eventually})
    1.14          |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
    1.15 -        |> fold (fn _ => fn thm => @{thm impI} RS thm) thms
    1.16 -      val cases_prop = Thm.prop_of (raw_elim_thm RS st)
    1.17 +        |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
    1.18 +      val cases_prop = Thm.prop_of (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal))
    1.19        val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
    1.20      in
    1.21 -      CASES cases (rtac raw_elim_thm 1)
    1.22 -    end) 1 st
    1.23 +      CASES cases (rtac raw_elim_thm i)
    1.24 +    end)
    1.25  *}
    1.26  
    1.27  method_setup eventually_elim = {*
    1.28 -  Scan.succeed (fn ctxt => METHOD_CASES (eventually_elim_tac ctxt))
    1.29 +  Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
    1.30  *} "elimination of eventually quantifiers"
    1.31  
    1.32