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