diff -r 96c68fd7ed46 -r f745ff8bdb91 indrule.ML
--- a/indrule.ML	Wed Sep 07 13:17:34 1994 +0200
+++ b/indrule.ML	Thu Sep 08 11:01:45 1994 +0200
@@ -68,7 +68,7 @@
 
 (*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);
@@ -82,8 +82,8 @@
       (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;
@@ -128,7 +128,7 @@
 	  (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;