indrule.ML

   in list_all_free (quantfrees, list_implies (iprems,concl)) end
   handle Bind => error"Recursion term not found in conclusion";
 
 (*Avoids backtracking by delivering the correct premise to each goal*)
 fun ind_tac [] 0 = all_tac
-  | ind_tac(prem::prems) i = REPEAT (ares_tac [Part_eqI,prem] i) THEN
+  | ind_tac(prem::prems) i = REPEAT (ares_tac [Part_eqI, prem, refl] i) THEN
 			     ind_tac prems (i-1);
 
 val pred = Free(pred_name, elem_type --> boolT);
 
 val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) intr_tms;

       (cterm_of sign (list_implies (ind_prems, 
 				    mk_tprop (mk_all_imp(big_rec_tm,pred)))))
       (fn prems =>
        [rtac (impI RS allI) 1,
 	etac raw_induct 1,
-	REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE, 
-					 ssubst])),
+	REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE] 
+			   ORELSE' hyp_subst_tac)),
 	REPEAT (FIRSTGOAL (eresolve_tac [PartE, CollectE])),
 	ind_tac (rev prems) (length prems)])
     handle e => print_sign_exn sign e;
 
 (*** Prove the simultaneous induction rule ***)

     prove_goalw_cterm part_rec_defs 
 	  (cterm_of sign (mk_implies (induct_concl,mutual_induct_concl)))
 	  (fn prems =>
 	   [cut_facts_tac prems 1,
 	    REPEAT (eresolve_tac [asm_rl, conjE, PartE, mp] 1
-	     ORELSE resolve_tac [allI, impI, conjI, Part_eqI] 1
+	     ORELSE resolve_tac [allI, impI, conjI, Part_eqI, refl] 1
 	     ORELSE dresolve_tac [spec, mp, splitD] 1)])
     handle e => print_sign_exn sign e;
 
 (*Mutual induction follows by freeness of Inl/Inr.*)