diff -r b87b14e885af -r 43f5dfb7fa35 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Jul 22 14:39:56 2022 +0200
@@ -1226,7 +1226,7 @@
 subsubsection \<open>Expressing set operations via \<^const>\<open>fold\<close>\<close>
 
 lemma comp_fun_commute_const: "comp_fun_commute (\<lambda>_. f)"
-  by standard rule
+  by standard (rule refl)
 
 lemma comp_fun_idem_insert: "comp_fun_idem insert"
   by standard auto
@@ -1571,7 +1571,7 @@
 
 global_interpretation card: folding "\<lambda>_. Suc" 0
   defines card = "folding_on.F (\<lambda>_. Suc) 0"
-  by standard rule
+  by standard (rule refl)
 
 lemma card_insert_disjoint: "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> card (insert x A) = Suc (card A)"
   by (fact card.insert)
@@ -1824,11 +1824,12 @@
     from "2.prems"(1,2,5) "2.hyps"(1,2) have cst: "card s \<le> card t"
       by simp
     from "2.prems"(3) [OF "2.hyps"(1) cst]
-    obtain f where "f ` s \<subseteq> t" "inj_on f s"
+    obtain f where *: "f ` s \<subseteq> t" "inj_on f s"
       by blast
-    with "2.prems"(2) "2.hyps"(2) show ?case
-      unfolding inj_on_def
-      by (rule_tac x = "\<lambda>z. if z = x then y else f z" in exI) auto
+    let ?g = "(\<lambda>a. if a = x then y else f a)"
+    have "?g ` insert x s \<subseteq> insert y t \<and> inj_on ?g (insert x s)"
+      using * "2.prems"(2) "2.hyps"(2) unfolding inj_on_def by auto
+    then show ?case by (rule exI[where ?x="?g"])
   qed
 qed
 
@@ -2415,7 +2416,7 @@
           by (simp add: fS)
         have "\<lbrakk>x \<noteq> y; x \<in> S; z \<in> S; f x = f y\<rbrakk>
          \<Longrightarrow> \<exists>x \<in> S. x \<noteq> y \<and> f z = f x" for z
-          by (case_tac "z = y \<longrightarrow> z = x") auto
+          by (cases "z = y \<longrightarrow> z = x") auto
         then show "T \<subseteq> f ` (S - {y})"
           using h xy x y f by fastforce
       qed