diff -r 09354d37a5ab -r ce37c64244c0 src/Provers/ind.ML
--- a/src/Provers/ind.ML	Fri Feb 16 17:24:51 1996 +0100
+++ b/src/Provers/ind.ML	Fri Feb 16 18:00:47 1996 +0100
@@ -40,22 +40,23 @@
 fun qnt_tac i = fn (tac,var) => tac THEN res_inst_tac [(a_name,var)] spec i;
 
 (*Generalizes over all free variables, with the named var outermost.*)
-fun all_frees_tac (var:string) i = Tactic(fn thm =>
+fun all_frees_tac (var:string) i thm = 
     let val tsig = #tsig(Sign.rep_sg(#sign(rep_thm thm)));
         val frees = add_term_frees tsig (nth_elem(i-1,prems_of thm),[var]);
         val frees' = sort(op>)(frees \ var) @ [var]
-    in tapply(foldl (qnt_tac i) (all_tac,frees'), thm) end);
+    in foldl (qnt_tac i) (all_tac,frees') thm end;
 
 fun REPEAT_SIMP_TAC simp_tac n i =
-let fun repeat thm = tapply(COND (has_fewer_prems n) all_tac
-	let val k = length(prems_of thm)
-	in simp_tac i THEN COND (has_fewer_prems k) (Tactic repeat) all_tac
-	end, thm)
-in Tactic repeat end;
+let fun repeat thm = 
+        (COND (has_fewer_prems n) all_tac
+	 let val k = nprems_of thm
+	 in simp_tac i THEN COND (has_fewer_prems k) repeat all_tac end)
+	thm
+in repeat end;
 
-fun ALL_IND_TAC sch simp_tac i = Tactic(fn thm => tapply(
-	resolve_tac [sch] i THEN
-	REPEAT_SIMP_TAC simp_tac (length(prems_of thm)) i, thm));
+fun ALL_IND_TAC sch simp_tac i thm = 
+	(resolve_tac [sch] i THEN
+	 REPEAT_SIMP_TAC simp_tac (nprems_of thm) i) thm;
 
 fun IND_TAC sch simp_tac var =
 	all_frees_tac var THEN' ALL_IND_TAC sch simp_tac;