src/HOL/List.thy

   from assms have 1: "length xs = length ys" by (auto dest!: distinct_card)
   from assms show ?thesis
   proof(induct rule:list_induct2[OF 1])
     case 1 show ?case by simp
   next
-    case 2 thus ?case by simp (metis Diff_insert_absorb antisym insertE insert_iff)
+    case (2 x xs y ys)
+    then show ?case
+      by (cases \<open>x = y\<close>) (auto simp add: insert_eq_iff)
   qed
 qed
 
 lemma map_sorted_distinct_set_unique:
   assumes "inj_on f (set xs \<union> set ys)"

 by (induct xs) simp_all
 
 lemma insort_key_left_comm:
   assumes "f x \<noteq> f y"
   shows "insort_key f y (insort_key f x xs) = insort_key f x (insort_key f y xs)"
-by (induct xs) (auto simp add: assms dest: antisym)
+by (induct xs) (auto simp add: assms dest: order.antisym)
 
 lemma insort_left_comm:
   "insort x (insort y xs) = insort y (insort x xs)"
 by (cases "x = y") (auto intro: insort_key_left_comm)