diff -r f99617e7103f -r 11cc1ccad58e src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu May 10 22:11:38 2007 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri May 11 00:43:45 2007 +0200
@@ -266,6 +266,6 @@
     qed
     finally show ?thesis .
   qed
-qed (simp_all! add: continuous_def)
+qed (insert `continuous V norm f`, simp_all add: continuous_def)
 
 end