diff -r d995733b635d -r f0de18b62d63 src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Library/Product_Vector.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -489,11 +489,11 @@
 
 subsection {* Pair operations are linear *}
 
-interpretation fst: bounded_linear fst
+lemma bounded_linear_fst: "bounded_linear fst"
   using fst_add fst_scaleR
   by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
 
-interpretation snd: bounded_linear snd
+lemma bounded_linear_snd: "bounded_linear snd"
   using snd_add snd_scaleR
   by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)