diff -r abb7d0bac7e0 -r c0e62be6ef04 indrule.ML
--- a/indrule.ML	Thu Oct 06 09:36:40 1994 +0100
+++ b/indrule.ML	Wed Oct 12 12:00:45 1994 +0100
@@ -68,8 +68,9 @@
 
 (*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, refl] i) THEN
-			     ind_tac prems (i-1);
+  | ind_tac(prem::prems) i = 
+	DEPTH_SOLVE_1 (ares_tac [Part_eqI, prem, refl] i) THEN
+	ind_tac prems (i-1);
 
 val pred = Free(pred_name, elem_type --> boolT);
 
@@ -140,15 +141,22 @@
 (*Avoids backtracking by delivering the correct premise to each goal*)
 fun mutual_ind_tac [] 0 = all_tac
   | mutual_ind_tac(prem::prems) i = 
-      SELECT_GOAL 
-	((*unpackage and use "prem" in the corresponding place*)
-	 REPEAT (FIRSTGOAL
-		    (eresolve_tac ([conjE,mp]@cmonos) ORELSE'
-		     ares_tac [prem,impI,conjI]))
-	 (*prove remaining goals by contradiction*)
-	 THEN rewrite_goals_tac (con_defs@part_rec_defs)
-	 THEN REPEAT (eresolve_tac (PartE :: sumprod_free_SEs) 1))
-	i  THEN mutual_ind_tac prems (i-1);
+      DETERM
+       (SELECT_GOAL 
+	  ((*unpackage and use "prem" in the corresponding place*)
+	   REPEAT (FIRSTGOAL
+		   (etac conjE ORELSE' eq_mp_tac ORELSE' 
+		    ares_tac [impI, conjI]))
+	   (*prem is not allowed in the REPEAT, lest it loop!*)
+	   THEN TRYALL (rtac prem)
+	   THEN REPEAT
+		  (FIRSTGOAL (ares_tac [impI] ORELSE' 
+			      eresolve_tac (mp::cmonos)))
+	   (*prove remaining goals by contradiction*)
+	   THEN rewrite_goals_tac (con_defs@part_rec_defs)
+	   THEN DEPTH_SOLVE (eresolve_tac (PartE :: sumprod_free_SEs) 1))
+	  i)
+	THEN mutual_ind_tac prems (i-1);
 
 val mutual_induct_split = 
     prove_goalw_cterm []