src/HOL/Data_Structures/Tree_Set.thy

 by (induction t) (auto simp: elems_simps2)
 
 
 lemma inorder_insert:
   "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
-by(induction t) (auto simp: ins_simps)
+by(induction t) (auto simp: ins_list_simps)
 
 
 lemma del_minD:
   "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted(inorder t) \<Longrightarrow>
    x # inorder t' = inorder t"
 by(induction t arbitrary: t' rule: del_min.induct)
   (auto simp: sorted_lems split: prod.splits)
 
 lemma inorder_delete:
   "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
-by(induction t) (auto simp: del_simps del_minD split: prod.splits)
+by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)
 
 
 interpretation Set_by_Ordered
 where empty = Leaf and isin = isin and insert = insert and delete = delete
 and inorder = inorder and wf = "\<lambda>_. True"