diff -r 0b70405b3969 -r 30486b96274d src/HOL/Data_Structures/Tree23_Set.thy
--- a/src/HOL/Data_Structures/Tree23_Set.thy	Thu Mar 22 17:18:33 2018 +0100
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Fri Mar 23 11:37:02 2018 +0100
@@ -142,11 +142,8 @@
 
 subsubsection "Proofs for isin"
 
-lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (induction t) (auto simp: elems_simps1 ball_Un)
-
-lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (induction t) (auto simp: elems_simps2)
+lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set (inorder t))"
+by (induction t) (auto simp: isin_simps ball_Un)
 
 
 subsubsection "Proofs for insert"