diff -r b87b14e885af -r 43f5dfb7fa35 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Quotient.thy	Fri Jul 22 14:39:56 2022 +0200
@@ -148,8 +148,8 @@
   moreover
   have "(R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" for a
     by (rule rel_funI)
-      (insert q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2],
-        simp (no_asm) add: Quotient3_def, simp)
+       (use q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2]
+         in \<open>simp (no_asm) add: Quotient3_def, simp\<close>)
   moreover
   have "(R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
         (rep1 ---> abs2) r  = (rep1 ---> abs2) s)" for r s
@@ -322,9 +322,9 @@
 
 lemma babs_rsp:
   assumes q: "Quotient3 R1 Abs1 Rep1"
-  and     a: "(R1 ===> R2) f g"
-  shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
-proof (clarsimp simp add: Babs_def in_respects rel_fun_def)
+      and a: "(R1 ===> R2) f g"
+    shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
+proof
   fix x y
   assume "R1 x y"
   then have "x \<in> Respects R1 \<and> y \<in> Respects R1"
@@ -542,7 +542,7 @@
       then have "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> Collect (R r) = Collect (R s)"
         by (metis abs_inverse)
       also have "Collect (R r) = Collect (R s) \<longleftrightarrow> (\<lambda>A x. x \<in> A) (Collect (R r)) = (\<lambda>A x. x \<in> A) (Collect (R s))"
-        by rule simp_all
+        by (rule iffI) simp_all
       finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" by simp
     qed
     then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))"