diff -r 5f3cffe16311 -r cebf36c14226 src/HOL/Data_Structures/Tree234_Set.thy
--- a/src/HOL/Data_Structures/Tree234_Set.thy	Sun May 06 23:59:14 2018 +0100
+++ b/src/HOL/Data_Structures/Tree234_Set.thy	Tue May 08 10:14:36 2018 +0200
@@ -9,6 +9,8 @@
   Set_Specs
 begin
 
+declare sorted_wrt.simps(2)[simp del]
+
 subsection \<open>Set operations on 2-3-4 trees\<close>
 
 fun isin :: "'a::linorder tree234 \<Rightarrow> 'a \<Rightarrow> bool" where