diff -r c5a8b612e571 -r 0040bafffdef src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Library/Product_Vector.thy	Thu Jul 01 16:54:44 2010 +0200
@@ -10,7 +10,7 @@
 
 subsection {* Product is a real vector space *}
 
-instantiation "*" :: (real_vector, real_vector) real_vector
+instantiation prod :: (real_vector, real_vector) real_vector
 begin
 
 definition scaleR_prod_def:
@@ -41,8 +41,7 @@
 
 subsection {* Product is a topological space *}
 
-instantiation
-  "*" :: (topological_space, topological_space) topological_space
+instantiation prod :: (topological_space, topological_space) topological_space
 begin
 
 definition open_prod_def:
@@ -157,8 +156,7 @@
 
 subsection {* Product is a metric space *}
 
-instantiation
-  "*" :: (metric_space, metric_space) metric_space
+instantiation prod :: (metric_space, metric_space) metric_space
 begin
 
 definition dist_prod_def:
@@ -340,7 +338,7 @@
 
 subsection {* Product is a complete metric space *}
 
-instance "*" :: (complete_space, complete_space) complete_space
+instance prod :: (complete_space, complete_space) complete_space
 proof
   fix X :: "nat \<Rightarrow> 'a \<times> 'b" assume "Cauchy X"
   have 1: "(\<lambda>n. fst (X n)) ----> lim (\<lambda>n. fst (X n))"
@@ -357,8 +355,7 @@
 
 subsection {* Product is a normed vector space *}
 
-instantiation
-  "*" :: (real_normed_vector, real_normed_vector) real_normed_vector
+instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector
 begin
 
 definition norm_prod_def:
@@ -397,11 +394,11 @@
 
 end
 
-instance "*" :: (banach, banach) banach ..
+instance prod :: (banach, banach) banach ..
 
 subsection {* Product is an inner product space *}
 
-instantiation "*" :: (real_inner, real_inner) real_inner
+instantiation prod :: (real_inner, real_inner) real_inner
 begin
 
 definition inner_prod_def: