diff -r 3f3223b90239 -r e051eea34990 src/HOL/Data_Structures/Tree23_Set.thy
--- a/src/HOL/Data_Structures/Tree23_Set.thy	Thu Jul 07 09:24:03 2016 +0200
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Thu Jul 07 18:08:02 2016 +0200
@@ -9,7 +9,7 @@
   Set_by_Ordered
 begin
 
-fun isin :: "'a::cmp tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
+fun isin :: "'a::linorder tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
 "isin Leaf x = False" |
 "isin (Node2 l a r) x =
   (case cmp x a of
@@ -32,7 +32,7 @@
 "tree\<^sub>i (T\<^sub>i t) = t" |
 "tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r"
 
-fun ins :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
+fun ins :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
 "ins x Leaf = Up\<^sub>i Leaf x Leaf" |
 "ins x (Node2 l a r) =
    (case cmp x a of
@@ -66,7 +66,7 @@
 
 hide_const insert
 
-definition insert :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
+definition insert :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
 "insert x t = tree\<^sub>i(ins x t)"
 
 datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23"
@@ -108,7 +108,7 @@
 "del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
 "del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))"
 
-fun del :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
+fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
 "del x Leaf = T\<^sub>d Leaf" |
 "del x (Node2 Leaf a Leaf) =
   (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" |
@@ -131,7 +131,7 @@
           EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
           GT \<Rightarrow> node33 l a m b (del x r)))"
 
-definition delete :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
+definition delete :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
 "delete x t = tree\<^sub>d(del x t)"