Better use the finite simproc selectively only

--- a/src/HOL/Finite_Set.thy	Fri Nov 04 20:56:07 2022 +0100
+++ b/src/HOL/Finite_Set.thy	Sat Nov 05 09:57:51 2022 +0100
@@ -222,6 +222,9 @@
 in proc end
 \<close>
 
+(* Needs to be used with care *)
+declare [[simproc del: finite]]
+
 lemma finite_UnI:
   assumes "finite F" and "finite G"
   shows "finite (F \<union> G)"