--- a/src/HOL/Data_Structures/Tree_Set.thy Tue Sep 22 14:31:22 2015 +0200
+++ b/src/HOL/Data_Structures/Tree_Set.thy Tue Sep 22 17:13:01 2015 +0200
@@ -35,10 +35,10 @@
subsection "Functional Correctness Proofs"
lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (induction t) (auto simp: elems_simps)
+by (induction t) (auto simp: elems_simps1)
lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (induction t) (auto simp: elems_simps0 dest: sortedD)
+by (induction t) (auto simp: elems_simps2)
lemma inorder_insert: