src/HOL/Set.thy

--- a/src/HOL/Set.thy	Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/Set.thy	Tue Feb 10 16:46:21 2015 +0100
@@ -75,7 +75,7 @@
       resolve_tac ctxt @{thms iffI} 1 THEN
       ALLGOALS
         (EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms conjE},
-          DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
+          DEPTH_SOLVE_1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms conjI})]))
 *}
 
 lemmas CollectE = CollectD [elim_format]