src/HOL/Filter.thy
changeset 60589 b5622eef7176
parent 60182 e1ea5a6379c9
child 60721 c1b7793c23a3
     1.1 --- a/src/HOL/Filter.thy	Fri Jun 26 14:53:15 2015 +0200
     1.2 +++ b/src/HOL/Filter.thy	Fri Jun 26 14:53:28 2015 +0200
     1.3 @@ -245,7 +245,9 @@
     1.4          (@{thm allI} RS @{thm always_eventually})
     1.5          |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
     1.6          |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
     1.7 -      val cases_prop = Thm.prop_of (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal))
     1.8 +      val cases_prop =
     1.9 +        Thm.prop_of
    1.10 +          (Rule_Cases.internalize_params (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal)))
    1.11        val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
    1.12      in
    1.13        CASES cases (rtac raw_elim_thm i)