# HG changeset patch
# User wenzelm
# Date 1521036526 -3600
# Node ID b9fae46f497b42a4c69827c289b96f5406a799cb
# Parent  8374c80165e1240902ef58b9a84c8f4013b90dfb
misc tuning and clarification;

diff -r 8374c80165e1 -r b9fae46f497b src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Tue Mar 13 21:54:48 2018 +0100
+++ b/src/HOL/Filter.thy	Wed Mar 14 15:08:46 2018 +0100
@@ -234,16 +234,15 @@
   fun eventually_elim_tac facts =
     CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
       let
-        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) facts
+        val mp_facts = facts RL @{thms eventually_rev_mp}
+        val rule =
+          @{thm eventuallyI}
+          |> fold (fn mp_fact => fn th => th RS mp_fact) mp_facts
+          |> funpow (length facts) (fn th => @{thm impI} RS th)
         val cases_prop =
-          Thm.prop_of
-            (Rule_Cases.internalize_params (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal)))
+          Thm.prop_of (Rule_Cases.internalize_params (rule RS Goal.init (Thm.cterm_of ctxt goal)))
         val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
-      in CONTEXT_CASES cases (resolve_tac ctxt [raw_elim_thm] i) (ctxt, st) end)
+      in CONTEXT_CASES cases (resolve_tac ctxt [rule] i) (ctxt, st) end)
 \<close>
 
 method_setup eventually_elim = \<open>