diff -r 5616fbda86e6 -r b16f976db515 src/HOL/Library/Quotient_Sum.thy
--- a/src/HOL/Library/Quotient_Sum.thy	Fri Dec 09 16:08:32 2011 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy	Fri Dec 09 18:07:04 2011 +0100
@@ -16,7 +16,7 @@
 | "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
 | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
 
-declare [[map sum = (sum_map, sum_rel)]]
+declare [[map sum = sum_rel]]
 
 lemma sum_rel_unfold:
   "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y