
diff -r 38598a19e701 -r 09bf8fcd1c6e src/HOL/Real/HahnBanach/FunctionNorm.thy
--- 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"




