diff -r f6b0d827240e -r bdc1e2f0a86a src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Tue Sep 01 17:25:36 2015 +0200
+++ b/src/HOL/Library/Mapping.thy	Tue Sep 01 22:32:58 2015 +0200
@@ -138,7 +138,7 @@
 
 subsection \<open>Derived operations\<close>
 
-definition ordered_keys :: "('a\<Colon>linorder, 'b) mapping \<Rightarrow> 'a list"
+definition ordered_keys :: "('a::linorder, 'b) mapping \<Rightarrow> 'a list"
 where
   "ordered_keys m = (if finite (keys m) then sorted_list_of_set (keys m) else [])"