--- a/src/HOL/Filter.thy Fri Jun 26 14:53:15 2015 +0200
+++ b/src/HOL/Filter.thy Fri Jun 26 14:53:28 2015 +0200
@@ -245,7 +245,9 @@
(@{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 cases_prop = Thm.prop_of (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal))
+ val cases_prop =
+ Thm.prop_of
+ (Rule_Cases.internalize_params (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal)))
val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
in
CASES cases (rtac raw_elim_thm i)
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri Jun 26 14:53:15 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Jun 26 14:53:28 2015 +0200
@@ -879,7 +879,7 @@
have "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y) \<le> (\<phi> x1 - \<phi> y) + e * \<bar>x1 - y\<bar>"
(is "\<forall>\<^sub>F x1 in ?F. ?le' x1")
proof eventually_elim
- case elim
+ case (elim x1)
from norm_triangle_ineq2[THEN order_trans, OF elim(1)]
have "norm (f x1 - f y) \<le> norm (f' y) * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
by (simp add: ac_simps)