# HG changeset patch
# User berghofe
# Date 1005557982 -3600
# Node ID dc67fdb03a2a27a0c172e647254ada78cc7a1e88
# Parent  46f128d8133c903dc199f6d2276bbfa6d9c14dfe
Fixed proof depending on strange behaviour of rename_bvs.

diff -r 46f128d8133c -r dc67fdb03a2a src/ZF/AC/DC.ML
--- a/src/ZF/AC/DC.ML	Mon Nov 12 10:37:36 2001 +0100
+++ b/src/ZF/AC/DC.ML	Mon Nov 12 10:39:42 2001 +0100
@@ -365,9 +365,8 @@
 by (rtac ballI 1);
 by (etac succE 1);
 (** LEVEL 25 **)
-by (dresolve_tac [domain_of_fun RSN (2, export f_n_pairs_in_R)] 2
-        THEN REPEAT (assume_tac 2));
-by (dtac bspec 2 THEN (assume_tac 2));
+by (EVERY [dtac (domain_of_fun RSN (2, export f_n_pairs_in_R)) 2,
+  REPEAT (assume_tac 2), dtac bspec 2, assume_tac 2]);
 by (asm_full_simp_tac (simpset()
         addsimps [nat_into_Ord RS succ_in_succ, succI2, cons_val_k]) 2);
 by (asm_full_simp_tac (simpset() addsimps [cons_val_n, cons_val_k]) 1);