src/HOL/Data_Structures/Tree23_Set.thy

--- a/src/HOL/Data_Structures/Tree23_Set.thy	Sun May 06 23:59:14 2018 +0100
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Tue May 08 10:14:36 2018 +0200
@@ -9,6 +9,8 @@
   Set_Specs
 begin
 
+declare sorted_wrt.simps(2)[simp del]
+
 fun isin :: "'a::linorder tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
 "isin Leaf x = False" |
 "isin (Node2 l a r) x =