--- a/src/HOL/Library/Quotient_Syntax.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Library/Quotient_Syntax.thy Thu Mar 06 15:40:33 2014 +0100
@@ -11,6 +11,6 @@
notation
rel_conj (infixr "OOO" 75) and
map_fun (infixr "--->" 55) and
- fun_rel (infixr "===>" 55)
+ rel_fun (infixr "===>" 55)
end