diff -r b87b14e885af -r 43f5dfb7fa35 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Wellfounded.thy	Fri Jul 22 14:39:56 2022 +0200
@@ -257,8 +257,10 @@
         then obtain z where "z \<in> Q" "(z, y) \<in> r\<^sup>*"
                             "\<And>z'. (z', z) \<in> r \<longrightarrow> z' \<in> Q \<longrightarrow> (z', y) \<notin> r\<^sup>*"
           using R' [of "{z \<in> Q. (z,y) \<in> r\<^sup>*}"] by auto
-        with R show ?thesis
-          by (rule_tac x="z" in bexI) (blast intro: rtrancl_trans)
+        then have "\<forall>y'. (y', z) \<in> insert (y, x) r \<longrightarrow> y' \<notin> Q"
+          using R by(blast intro: rtrancl_trans)+
+        then show ?thesis
+          by (rule bexI) fact
       next
         case False
         then show ?thesis
@@ -293,7 +295,7 @@
     thus ?thesis
       using inj unfolding A_def
       by (intro bexI[of _ "f a0"]) auto
-  qed (insert \<open>b \<in> B\<close>, unfold A_def, auto)
+  qed (use \<open>b \<in> B\<close> in  \<open>unfold A_def, auto\<close>)
 qed
 
 lemma wf_map_prod_image: "wf r \<Longrightarrow> inj f \<Longrightarrow> wf (map_prod f f ` r)"
@@ -581,11 +583,13 @@
   unfolding less_eq rtrancl_eq_or_trancl by auto
 
 lemma wf_pred_nat: "wf pred_nat"
-  apply (unfold wf_def pred_nat_def)
-  apply clarify
-  apply (induct_tac x)
-   apply blast+
-  done
+  unfolding wf_def
+proof clarify
+  fix P x
+  assume "\<forall>x'. (\<forall>y. (y, x') \<in> pred_nat \<longrightarrow> P y) \<longrightarrow> P x'"
+  then show "P x"
+    unfolding pred_nat_def by (induction x) blast+
+qed
 
 lemma wf_less_than [iff]: "wf less_than"
   by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])
@@ -673,10 +677,12 @@
   by (blast dest: accp_downwards_aux)
 
 theorem accp_wfPI: "\<forall>x. accp r x \<Longrightarrow> wfP r"
-  apply (rule wfPUNIVI)
-  apply (rule_tac P = P in accp_induct)
-   apply blast+
-  done
+proof (rule wfPUNIVI)
+  fix P x
+  assume "\<forall>x. accp r x" "\<forall>x. (\<forall>y. r y x \<longrightarrow> P y) \<longrightarrow> P x"
+  then show "P x"
+    using accp_induct[where P = P] by blast
+qed
 
 theorem accp_wfPD: "wfP r \<Longrightarrow> accp r x"
   apply (erule wfP_induct_rule)
@@ -750,15 +756,20 @@
   fixes f :: "'a \<Rightarrow> 'b"
   assumes "wf r"
   shows "wf (inv_image r f)"
-proof (clarsimp simp: inv_image_def wf_eq_minimal)
-  fix P and x::'a
-  assume "x \<in> P"
-  then obtain w where w: "w \<in> {w. \<exists>x::'a. x \<in> P \<and> f x = w}"
-    by auto
-  have *: "\<And>Q u. u \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q"
-    using assms by (auto simp add: wf_eq_minimal)
-  show "\<exists>z\<in>P. \<forall>y. (f y, f z) \<in> r \<longrightarrow> y \<notin> P"
-    using * [OF w] by auto
+proof -
+  have "\<And>x P. x \<in> P \<Longrightarrow> \<exists>z\<in>P. \<forall>y. (f y, f z) \<in> r \<longrightarrow> y \<notin> P"
+  proof -
+    fix P and x::'a
+    assume "x \<in> P"
+    then obtain w where w: "w \<in> {w. \<exists>x::'a. x \<in> P \<and> f x = w}"
+      by auto
+    have *: "\<And>Q u. u \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q"
+      using assms by (auto simp add: wf_eq_minimal)
+    show "\<exists>z\<in>P. \<forall>y. (f y, f z) \<in> r \<longrightarrow> y \<notin> P"
+      using * [OF w] by auto
+  qed
+  then show ?thesis
+    by (clarsimp simp: inv_image_def wf_eq_minimal)
 qed
 
 text \<open>Measure functions into \<^typ>\<open>nat\<close>\<close>
@@ -901,7 +912,7 @@
         next
           case False
           from * finites have N2: "(?N2, M) \<in> max_ext r"
-            by (rule_tac max_extI[OF _ _ \<open>M \<noteq> {}\<close>]) auto
+            using max_extI[OF _ _ \<open>M \<noteq> {}\<close>, where ?X = ?N2] by auto
           with \<open>M \<in> ?W\<close> show "?N2 \<in> ?W" by (rule acc_downward)
         qed
         with finites have "?N1 \<union> ?N2 \<in> ?W"