src/HOL/Library/Quotient_Syntax.thy
changeset 40602 91e583511113
parent 35787 afdf1c4958b2
child 55945 e96383acecf9
--- 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