--- a/src/HOL/Analysis/Connected.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Analysis/Connected.thy Thu Jul 08 08:42:36 2021 +0200
@@ -240,7 +240,7 @@
\<Longrightarrow> connected_component_set S x = connected_component_set S y"
apply (simp add: ex_in_conv [symmetric])
apply (rule connected_component_eq)
-by (metis (no_types, hide_lams) connected_component_eq_eq connected_component_in connected_component_maximal subsetD mem_Collect_eq)
+by (metis (no_types, opaque_lifting) connected_component_eq_eq connected_component_in connected_component_maximal subsetD mem_Collect_eq)
lemma Union_connected_component: "\<Union>(connected_component_set S ` S) = S"
@@ -335,7 +335,7 @@
by simp
lemma connected_eq_connected_components_eq: "connected s \<longleftrightarrow> (\<forall>c \<in> components s. \<forall>c' \<in> components s. c = c')"
- by (metis (no_types, hide_lams) components_iff connected_component_eq_eq connected_iff_connected_component)
+ by (metis (no_types, opaque_lifting) components_iff connected_component_eq_eq connected_iff_connected_component)
lemma components_eq_sing_iff: "components s = {s} \<longleftrightarrow> connected s \<and> s \<noteq> {}"
apply (rule iffI)