# HG changeset patch
# User lcp
# Date 784546975 -3600
# Node ID b71b6be593544d4cb8b65d752f3c3f9173a925ce
# Parent  3a5cd288358123f2c7d2833a2db8c74c87276dbe
Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.

diff -r 3a5cd2883581 -r b71b6be59354 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Fri Nov 11 10:41:09 1994 +0100
+++ b/src/Provers/hypsubst.ML	Fri Nov 11 10:42:55 1994 +0100
@@ -29,10 +29,6 @@
 
 local open Data in
 
-fun REPEATN 0 tac = all_tac
-  | REPEATN n tac = Tactic(fn state =>
-                           tapply(tac THEN REPEATN (n-1) tac,  state));
-
 exception EQ_VAR;
 
 fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]);
@@ -73,11 +69,11 @@
 	  val n = length(Logic.strip_assums_hyp Bi) - 1
 	  val (k,symopt) = eq_var bnd Bi
       in 
-	 EVERY [REPEATN k (etac rev_mp i),
+	 EVERY [REPEAT_DETERM_N k (etac rev_mp i),
 		etac revcut_rl i,
-		REPEATN (n-k) (etac rev_mp i),
+		REPEAT_DETERM_N (n-k) (etac rev_mp i),
 		etac (symopt RS subst) i,
-		REPEATN n (rtac imp_intr i)]
+		REPEAT_DETERM_N n (rtac imp_intr i)]
       end
       handle THM _ => no_tac | EQ_VAR => no_tac));