Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
authorlcp
Fri Nov 11 10:42:55 1994 +0100 (1994-11-11 ago)
changeset 704b71b6be59354
parent 703 3a5cd2883581
child 705 9fb068497df4
Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
src/Provers/hypsubst.ML
     1.1 --- a/src/Provers/hypsubst.ML	Fri Nov 11 10:41:09 1994 +0100
     1.2 +++ b/src/Provers/hypsubst.ML	Fri Nov 11 10:42:55 1994 +0100
     1.3 @@ -29,10 +29,6 @@
     1.4  
     1.5  local open Data in
     1.6  
     1.7 -fun REPEATN 0 tac = all_tac
     1.8 -  | REPEATN n tac = Tactic(fn state =>
     1.9 -                           tapply(tac THEN REPEATN (n-1) tac,  state));
    1.10 -
    1.11  exception EQ_VAR;
    1.12  
    1.13  fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]);
    1.14 @@ -73,11 +69,11 @@
    1.15  	  val n = length(Logic.strip_assums_hyp Bi) - 1
    1.16  	  val (k,symopt) = eq_var bnd Bi
    1.17        in 
    1.18 -	 EVERY [REPEATN k (etac rev_mp i),
    1.19 +	 EVERY [REPEAT_DETERM_N k (etac rev_mp i),
    1.20  		etac revcut_rl i,
    1.21 -		REPEATN (n-k) (etac rev_mp i),
    1.22 +		REPEAT_DETERM_N (n-k) (etac rev_mp i),
    1.23  		etac (symopt RS subst) i,
    1.24 -		REPEATN n (rtac imp_intr i)]
    1.25 +		REPEAT_DETERM_N n (rtac imp_intr i)]
    1.26        end
    1.27        handle THM _ => no_tac | EQ_VAR => no_tac));
    1.28