src/HOL/Topological_Spaces.thy
changeset 59970 e9f73d87d904
parent 59582 0fbed69ff081
child 59971 ea06500bb092
     1.1 --- a/src/HOL/Topological_Spaces.thy	Wed Apr 08 16:24:22 2015 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Apr 08 19:39:08 2015 +0200
     1.3 @@ -445,14 +445,13 @@
     1.4  ML {*
     1.5    fun eventually_elim_tac ctxt thms = SUBGOAL_CASES (fn (_, _, st) =>
     1.6      let
     1.7 -      val thy = Proof_Context.theory_of ctxt
     1.8        val mp_thms = thms RL [@{thm eventually_rev_mp}]
     1.9        val raw_elim_thm =
    1.10          (@{thm allI} RS @{thm always_eventually})
    1.11          |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
    1.12          |> fold (fn _ => fn thm => @{thm impI} RS thm) thms
    1.13        val cases_prop = Thm.prop_of (raw_elim_thm RS st)
    1.14 -      val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])])
    1.15 +      val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
    1.16      in
    1.17        CASES cases (rtac raw_elim_thm 1)
    1.18      end) 1