src/HOL/Library/DAList.thy

--- a/src/HOL/Library/DAList.thy	Sun Nov 26 13:19:52 2017 +0100
+++ b/src/HOL/Library/DAList.thy	Sun Nov 26 21:08:32 2017 +0100
@@ -22,7 +22,7 @@
 typedef ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct \<circ> map fst) xs}"
   morphisms impl_of Alist
 proof
-  show "[] \<in> {xs. (distinct o map fst) xs}"
+  show "[] \<in> {xs. (distinct \<circ> map fst) xs}"
     by simp
 qed