src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/HOL.thy	Wed Apr 08 19:39:08 2015 +0200
@@ -848,7 +848,7 @@
 apply (rule prem)
 apply assumption
 apply (rule allI)+
-apply (tactic {* eresolve_tac @{context} [Classical.dup_elim NONE @{thm allE}] 1 *})
+apply (tactic {* eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1 *})
 apply iprover
 done