# HG changeset patch
# User wenzelm
# Date 1435323208 -7200
# Node ID b5622eef7176df34c3e18d7fac0f72c476baad1d
# Parent  750c533459b1a7781055eae2cc3ee11e7ca7c44a
do not expose goal parameters;

diff -r 750c533459b1 -r b5622eef7176 src/HOL/Filter.thy
--- 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)
diff -r 750c533459b1 -r b5622eef7176 src/HOL/Multivariate_Analysis/Derivative.thy
--- 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)