fixed someI2_ex;

--- a/src/HOL/HOL_lemmas.ML	Fri Sep 15 20:20:45 2000 +0200
+++ b/src/HOL/HOL_lemmas.ML	Fri Sep 15 20:22:00 2000 +0200
@@ -373,7 +373,7 @@
 val [major,minor] = Goal "[| EX a. P a;  !!x. P x ==> Q x |] ==> Q (Eps P)";
 by (rtac (major RS exE) 1);
 by (etac someI2 1 THEN etac minor 1);
-qed "someI2EX";
+qed "someI2_ex";
 
 val prems = Goal
     "[| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a";

--- a/src/HOL/MicroJava/JVM/Store.ML	Fri Sep 15 20:20:45 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Store.ML	Fri Sep 15 20:22:00 2000 +0200
@@ -6,5 +6,5 @@
 
 Goalw [newref_def]
  "hp x = None \\<longrightarrow> hp (newref hp) = None";
-by (fast_tac (claset() addIs [someI2EX] addss (simpset())) 1);
+by (fast_tac (claset() addIs [someI2_ex] addss (simpset())) 1);
 qed_spec_mp "newref_None";

--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Sep 15 20:20:45 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Sep 15 20:22:00 2000 +0200
@@ -97,7 +97,7 @@
   "[| is_normed_vectorspace V norm; is_continuous V norm f|]
      ==> is_function_norm f V norm \<parallel>f\<parallel>V,norm" 
 proof (unfold function_norm_def is_function_norm_def 
-  is_continuous_def Sup_def, elim conjE, rule someI2EX)
+  is_continuous_def Sup_def, elim conjE, rule someI2_ex)
   assume "is_normed_vectorspace V norm"
   assume "is_linearform V f" 
   and e: "\<exists>c. \<forall>x \<in> V. |f x| <= c * norm x"

--- 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";