src/HOL/Topological_Spaces.thy
changeset 59971 ea06500bb092
parent 59970 e9f73d87d904
child 59976 046399298519
     1.1 --- a/src/HOL/Topological_Spaces.thy	Wed Apr 08 19:39:08 2015 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Apr 08 19:58:52 2015 +0200
     1.3 @@ -443,7 +443,7 @@
     1.4  qed
     1.5  
     1.6  ML {*
     1.7 -  fun eventually_elim_tac ctxt thms = SUBGOAL_CASES (fn (_, _, st) =>
     1.8 +  fun eventually_elim_tac ctxt thms st = SUBGOAL_CASES (fn _ =>
     1.9      let
    1.10        val mp_thms = thms RL [@{thm eventually_rev_mp}]
    1.11        val raw_elim_thm =
    1.12 @@ -454,7 +454,7 @@
    1.13        val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
    1.14      in
    1.15        CASES cases (rtac raw_elim_thm 1)
    1.16 -    end) 1
    1.17 +    end) 1 st
    1.18  *}
    1.19  
    1.20  method_setup eventually_elim = {*