src/HOL/Real/HahnBanach/NormedSpace.thy

--- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Thu Sep 14 15:51:20 2006 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Thu Sep 14 19:18:10 2006 +0200
@@ -15,8 +15,6 @@
   definite, absolute homogenous and subadditive.
 *}
 
-no_syntax norm :: "'a::norm \<Rightarrow> real" ("\<parallel>_\<parallel>")   (* FIXME clash with Real/RealVector.thy *)
-
 locale norm_syntax =
   fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")