src/HOL/Analysis/Abstract_Topology.thy

   shows "continuous_map X' X'' g"
   unfolding quotient_map_def continuous_map_def
 proof (intro conjI ballI allI impI)
   show "\<And>x'. x' \<in> topspace X' \<Longrightarrow> g x' \<in> topspace X''"
     using assms unfolding quotient_map_def
-    by (metis (no_types, hide_lams) continuous_map_image_subset_topspace image_comp image_subset_iff)
+    by (metis (no_types, opaque_lifting) continuous_map_image_subset_topspace image_comp image_subset_iff)
 next
   fix U'' :: "'c set"
   assume U'': "openin X'' U''"
   have "f ` topspace X = topspace X'"
     by (simp add: f quotient_imp_surjective_map)

    "retraction_map X Y f \<Longrightarrow> f ` (topspace X) = topspace Y"
   by (simp add: retraction_imp_quotient_map quotient_imp_surjective_map)
 
 lemma section_imp_injective_map:
    "\<lbrakk>section_map X Y f; x \<in> topspace X; y \<in> topspace X\<rbrakk> \<Longrightarrow> f x = f y \<longleftrightarrow> x = y"
-  by (metis (mono_tags, hide_lams) retraction_maps_def section_map_def)
+  by (metis (mono_tags, opaque_lifting) retraction_maps_def section_map_def)
 
 lemma retraction_maps_to_retract_maps:
    "retraction_maps X Y r s
         \<Longrightarrow> retraction_maps X (subtopology X (s ` (topspace Y))) (s \<circ> r) id"
   unfolding retraction_maps_def