src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/HOL.thy	Tue Feb 10 16:46:21 2015 +0100
@@ -904,7 +904,8 @@
   shows R
 apply (rule ex1E [OF major])
 apply (rule prem)
-apply (tactic {* ares_tac @{thms allI} 1 *})+
+apply assumption
+apply (rule allI)+
 apply (tactic {* eresolve_tac @{context} [Classical.dup_elim NONE @{thm allE}] 1 *})
 apply iprover
 done