src/HOL/Library/Enum.thy

--- a/src/HOL/Library/Enum.thy	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Library/Enum.thy	Thu Jul 01 16:54:44 2010 +0200
@@ -209,7 +209,7 @@
   using assms by (induct xs)
     (auto intro: inj_onI simp add: product_list_set distinct_map)
 
-instantiation * :: (enum, enum) enum
+instantiation prod :: (enum, enum) enum
 begin
 
 definition
@@ -220,7 +220,7 @@
 
 end
 
-instantiation "+" :: (enum, enum) enum
+instantiation sum :: (enum, enum) enum
 begin
 
 definition