--- a/src/HOL/Data_Structures/Splay_Set.thy Thu Jul 07 09:24:03 2016 +0200
+++ b/src/HOL/Data_Structures/Splay_Set.thy Thu Jul 07 18:08:02 2016 +0200
@@ -51,7 +51,7 @@
"\<lbrakk> x = x'; y = y'; z = z' \<rbrakk> \<Longrightarrow> case_tree x y z = case_tree x' y' z'"
by auto
-lemma splay_code: "splay (x::_::cmp) t = (case t of Leaf \<Rightarrow> Leaf |
+lemma splay_code: "splay (x::_::linorder) t = (case t of Leaf \<Rightarrow> Leaf |
Node al a ar \<Rightarrow> (case cmp x a of
EQ \<Rightarrow> t |
LT \<Rightarrow> (case al of
@@ -83,7 +83,7 @@
hide_const (open) insert
-fun insert :: "'a::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
"insert x t =
(if t = Leaf then Node Leaf x Leaf
else case splay x t of