src/HOL/Analysis/Bounded_Linear_Function.thy

--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Sat Oct 28 21:26:51 2017 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Sat Oct 28 23:32:37 2017 +0200
@@ -210,7 +210,7 @@
 end
 
 
-instance blinfun :: (banach, banach) banach
+instance blinfun :: (real_normed_vector, banach) banach
 proof
   fix X::"nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   assume "Cauchy X"