src/HOL/HOL.thy
changeset 59970 e9f73d87d904
parent 59940 087d81f5213e
child 59990 a81dc82ecba3
     1.1 --- a/src/HOL/HOL.thy	Wed Apr 08 16:24:22 2015 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Apr 08 19:39:08 2015 +0200
     1.3 @@ -848,7 +848,7 @@
     1.4  apply (rule prem)
     1.5  apply assumption
     1.6  apply (rule allI)+
     1.7 -apply (tactic {* eresolve_tac @{context} [Classical.dup_elim NONE @{thm allE}] 1 *})
     1.8 +apply (tactic {* eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1 *})
     1.9  apply iprover
    1.10  done
    1.11