reverted simprule status on a new lemma

--- a/src/HOL/Algebra/Free_Abelian_Groups.thy	Mon Mar 01 14:47:08 2021 +0000
+++ b/src/HOL/Algebra/Free_Abelian_Groups.thy	Mon Mar 01 17:59:17 2021 +0000
@@ -682,7 +682,7 @@
           by (auto simp: PiE_def Pi_def in_keys_iff)
         then show "(\<lambda>i\<in>I. Abs_poly_mapping (?f i))
                  \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. {c. Poly_Mapping.keys c \<subseteq> S i}. finite {i \<in> I. x i \<noteq> 0}}"
-          using fin unfolding J_def by (simp add: eq in_keys_iff cong: conj_cong)
+          using fin unfolding J_def by (force simp add: eq in_keys_iff cong: conj_cong)
       qed
     qed
     then show "carrier ?H \<subseteq> ?h ` carrier ?G"

--- a/src/HOL/Library/FuncSet.thy	Mon Mar 01 14:47:08 2021 +0000
+++ b/src/HOL/Library/FuncSet.thy	Mon Mar 01 17:59:17 2021 +0000
@@ -73,7 +73,7 @@
 
 lemma Pi_eq_empty[simp]: "(\<Pi> x \<in> A. B x) = {} \<longleftrightarrow> (\<exists>x\<in>A. B x = {})"
 proof -
-  have "\<exists>x\<in>A. B x = {}" if "\<And>f. \<exists>y. y \<in> A \<and> f y \<notin> B y" 
+  have "\<exists>x\<in>A. B x = {}" if "\<And>f. \<exists>y. y \<in> A \<and> f y \<notin> B y"
     using that [of "\<lambda>u. SOME y. y \<in> B u"] some_in_eq by blast
   then show ?thesis
     by force
@@ -432,7 +432,7 @@
 lemma PiE_iff: "f \<in> Pi\<^sub>E I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i) \<and> f \<in> extensional I"
   by (simp add: PiE_def Pi_iff)
 
-lemma restrict_PiE_iff [simp]: "restrict f I \<in> Pi\<^sub>E I X \<longleftrightarrow> (\<forall>i \<in> I. f i \<in> X i)"
+lemma restrict_PiE_iff: "restrict f I \<in> Pi\<^sub>E I X \<longleftrightarrow> (\<forall>i \<in> I. f i \<in> X i)"
   by (simp add: PiE_iff)
 
 lemma ext_funcset_to_sing_iff [simp]: "A \<rightarrow>\<^sub>E {a} = {\<lambda>x\<in>A. a}"
@@ -537,7 +537,7 @@
     by auto
 qed
 
-lemma PiE_singleton: 
+lemma PiE_singleton:
   assumes "f \<in> extensional A"
   shows   "PiE A (\<lambda>x. {f x}) = {f}"
 proof -