diff -r c5a8b612e571 -r 0040bafffdef src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jul 01 16:54:44 2010 +0200
@@ -5,7 +5,7 @@
 imports Finite_Cartesian_Product Integration
 begin
 
-instantiation * :: (real_basis, real_basis) real_basis
+instantiation prod :: (real_basis, real_basis) real_basis
 begin
 
 definition "basis i = (if i < DIM('a) then (basis i, 0) else (0, basis (i - DIM('a))))"
@@ -131,7 +131,7 @@
 lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('b::real_basis) + DIM('a::real_basis)"
   by (rule dimension_eq) (auto simp: basis_prod_def zero_prod_def basis_eq_0_iff)
 
-instance * :: (euclidean_space, euclidean_space) euclidean_space
+instance prod :: (euclidean_space, euclidean_space) euclidean_space
 proof (default, safe)
   let ?b = "basis :: nat \<Rightarrow> 'a \<times> 'b"
   fix i j assume "i < DIM('a \<times> 'b)" "j < DIM('a \<times> 'b)"
@@ -139,7 +139,7 @@
     unfolding basis_prod_def by (auto simp: dot_basis)
 qed
 
-instantiation * :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
+instantiation prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
 begin
 
 definition "x \<le> (y::('a\<times>'b)) \<longleftrightarrow> (\<forall>i<DIM('a\<times>'b). x $$ i \<le> y $$ i)"