src/HOL/Library/RBT_Mapping.thy

--- a/src/HOL/Library/RBT_Mapping.thy	Tue Sep 01 17:25:36 2015 +0200
+++ b/src/HOL/Library/RBT_Mapping.thy	Tue Sep 01 22:32:58 2015 +0200
@@ -12,7 +12,7 @@
 subsection \<open>Implementation of mappings\<close>
 
 context includes rbt.lifting begin
-lift_definition Mapping :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" is RBT.lookup .
+lift_definition Mapping :: "('a::linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" is RBT.lookup .
 end
 
 code_datatype Mapping