diff -r d81d57979771 -r dbad46932536 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Fri Aug 19 15:07:10 2011 -0700
+++ b/src/HOL/Deriv.thy	Fri Aug 19 15:54:43 2011 -0700
@@ -524,7 +524,7 @@
                 ((\<forall>n. l \<le> g(n)) & g ----> l)"
 apply (drule lemma_nest, auto)
 apply (subgoal_tac "l = m")
-apply (drule_tac [2] X = f in LIMSEQ_diff)
+apply (drule_tac [2] f = f in LIMSEQ_diff)
 apply (auto intro: LIMSEQ_unique)
 done