src/HOL/Tools/inductive.ML

              rewrite_goals_tac ctxt4 rec_preds_defs,
              dresolve_tac ctxt4 [unfold RS iffD1] 1,
              REPEAT (FIRSTGOAL (eresolve_tac ctxt4 rules1)),
              REPEAT (FIRSTGOAL (eresolve_tac ctxt4 rules2)),
              EVERY (map (fn prem =>
-               DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt4 rec_preds_defs prem, conjI] 1))
+               DEPTH_SOLVE_1 (assume_tac ctxt4 1 ORELSE
+                resolve_tac ctxt [rewrite_rule ctxt4 rec_preds_defs prem, conjI] 1))
                 (tl prems))])
           |> singleton (Proof_Context.export ctxt'' ctxt'''),
          map #2 c_intrs, length Ts)
       end
 

            some premise involves disjunction.*)
          REPEAT (FIRSTGOAL (eresolve_tac ctxt3 [conjE] ORELSE' bound_hyp_subst_tac ctxt3)),
          REPEAT (FIRSTGOAL
            (resolve_tac ctxt3 [conjI, impI] ORELSE'
            (eresolve_tac ctxt3 [notE] THEN' assume_tac ctxt3))),
-         EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt3
-             (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
-           conjI, refl] 1)) prems)]);
+         EVERY (map (fn prem =>
+            DEPTH_SOLVE_1 (assume_tac ctxt3 1 ORELSE
+              resolve_tac ctxt3
+                [rewrite_rule ctxt3 (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
+                  conjI, refl] 1)) prems)]);
 
     val lemma = Goal.prove_sorry ctxt'' [] []
       (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn {context = ctxt3, ...} => EVERY
         [rewrite_goals_tac ctxt3 rec_preds_defs,
          REPEAT (EVERY