src/HOL/Filter.thy
changeset 60752 b48830b670a1
parent 60721 c1b7793c23a3
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Filter.thy	Sat Jul 18 20:37:16 2015 +0200
     1.2 +++ b/src/HOL/Filter.thy	Sat Jul 18 20:47:08 2015 +0200
     1.3 @@ -250,7 +250,7 @@
     1.4            (Rule_Cases.internalize_params (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal)))
     1.5        val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
     1.6      in
     1.7 -      CASES cases (rtac raw_elim_thm i)
     1.8 +      CASES cases (resolve_tac ctxt [raw_elim_thm] i)
     1.9      end)
    1.10  *}
    1.11