--- a/src/HOL/Library/RBT_Set.thy Tue Sep 01 17:25:36 2015 +0200
+++ b/src/HOL/Library/RBT_Set.thy Tue Sep 01 22:32:58 2015 +0200
@@ -18,10 +18,10 @@
section \<open>Definition of code datatype constructors\<close>
-definition Set :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set"
+definition Set :: "('a::linorder, unit) rbt \<Rightarrow> 'a set"
where "Set t = {x . RBT.lookup t x = Some ()}"
-definition Coset :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set"
+definition Coset :: "('a::linorder, unit) rbt \<Rightarrow> 'a set"
where [simp]: "Coset t = - Set t"