diff -r 16742772a9b3 -r 91e583511113 src/HOL/Library/Quotient_Syntax.thy
--- a/src/HOL/Library/Quotient_Syntax.thy	Thu Nov 18 12:37:30 2010 +0100
+++ b/src/HOL/Library/Quotient_Syntax.thy	Thu Nov 18 17:01:15 2010 +0100
@@ -10,7 +10,7 @@
 
 notation
   rel_conj (infixr "OOO" 75) and
-  fun_map (infixr "--->" 55) and
+  map_fun (infixr "--->" 55) and
   fun_rel (infixr "===>" 55)
 
 end