diff -r 54f186bb5e3e -r 3b21b24a5fb6 Quot/QuotSum.thy
--- a/Quot/QuotSum.thy	Tue Dec 22 22:10:48 2009 +0100
+++ b/Quot/QuotSum.thy	Wed Dec 23 10:31:54 2009 +0100
@@ -16,7 +16,8 @@
   "sum_map f1 f2 (Inl a) = Inl (f1 a)"
 | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
 
-declare [[map * = (sum_map, sum_rel)]]
+declare [[map "+" = (sum_map, sum_rel)]]
+
 
 lemma sum_equivp[quot_equiv]:
   assumes a: "equivp R1"