diff -r 59203adfc33f -r ccda99401bc8 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Thu Oct 30 22:45:19 2014 +0100
@@ -75,11 +75,14 @@
               SOME (close (Goal.prove ctxt [] [])
                 (Logic.mk_equals (t, fold_rev Term.abs xs (m $ p $ (bop $ S $ S'))))
                 (K (EVERY
-                  [rtac eq_reflection 1, REPEAT (rtac @{thm ext} 1), rtac iffI 1,
-                   EVERY [etac conjE 1, rtac IntI 1, simp, simp,
-                     etac IntE 1, rtac conjI 1, simp, simp] ORELSE
-                   EVERY [etac disjE 1, rtac UnI1 1, simp, rtac UnI2 1, simp,
-                     etac UnE 1, rtac disjI1 1, simp, rtac disjI2 1, simp]])))
+                  [resolve_tac [eq_reflection] 1, REPEAT (resolve_tac @{thms ext} 1),
+                   resolve_tac [iffI] 1,
+                   EVERY [eresolve_tac [conjE] 1, resolve_tac [IntI] 1, simp, simp,
+                     eresolve_tac [IntE] 1, resolve_tac [conjI] 1, simp, simp] ORELSE
+                   EVERY [eresolve_tac [disjE] 1, resolve_tac [UnI1] 1, simp,
+                     resolve_tac [UnI2] 1, simp,
+                     eresolve_tac [UnE] 1, resolve_tac [disjI1] 1, simp,
+                     resolve_tac [disjI2] 1, simp]])))
                 handle ERROR _ => NONE))
     in
       case strip_comb t of
@@ -502,8 +505,9 @@
                fold_rev (Term.abs o pair "x") Ts
                 (HOLogic.mk_mem (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
                   list_comb (c, params))))))
-            (K (REPEAT (rtac @{thm ext} 1) THEN simp_tac (put_simpset HOL_basic_ss lthy addsimps
-              [def, mem_Collect_eq, @{thm split_conv}]) 1))
+            (K (REPEAT (resolve_tac @{thms ext} 1) THEN
+              simp_tac (put_simpset HOL_basic_ss lthy addsimps
+                [def, mem_Collect_eq, @{thm split_conv}]) 1))
         in
           lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
             [Attrib.internal (K pred_set_conv_att)]),