--- a/src/HOL/Topological_Spaces.thy Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy Wed Apr 08 19:39:08 2015 +0200
@@ -445,14 +445,13 @@
ML {*
fun eventually_elim_tac ctxt thms = SUBGOAL_CASES (fn (_, _, st) =>
let
- val thy = Proof_Context.theory_of ctxt
val mp_thms = thms RL [@{thm 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)
- val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])])
+ val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
in
CASES cases (rtac raw_elim_thm 1)
end) 1