src/HOL/WF_Rel.ML

--- a/src/HOL/WF_Rel.ML	Fri Sep 15 20:20:45 2000 +0200
+++ b/src/HOL/WF_Rel.ML	Fri Sep 15 20:22:00 2000 +0200
@@ -150,14 +150,14 @@
  by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
  by (rtac allI 1);
  by (Simp_tac 1);
- by (rtac someI2EX 1);
+ by (rtac someI2_ex 1);
   by (Blast_tac 1);
  by (Blast_tac 1);
 by (rtac allI 1);
 by (induct_tac "n" 1);
  by (Asm_simp_tac 1);
 by (Simp_tac 1);
-by (rtac someI2EX 1);
+by (rtac someI2_ex 1);
  by (Blast_tac 1);
 by (Blast_tac 1);
 qed "wf_iff_no_infinite_down_chain";