diff -r 5616fbda86e6 -r b16f976db515 src/HOL/Library/Quotient_Product.thy
--- a/src/HOL/Library/Quotient_Product.thy	Fri Dec 09 16:08:32 2011 +0100
+++ b/src/HOL/Library/Quotient_Product.thy	Fri Dec 09 18:07:04 2011 +0100
@@ -13,7 +13,7 @@
 where
   "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
 
-declare [[map prod = (map_pair, prod_rel)]]
+declare [[map prod = prod_rel]]
 
 lemma prod_rel_apply [simp]:
   "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"