changeset 73932 | fd21b4a93043 |
parent 73348 | 65c45cba3f54 |
child 75078 | ec86cb2418e1 |
--- a/src/HOL/Library/FuncSet.thy Fri Jun 18 15:03:12 2021 +0200 +++ b/src/HOL/Library/FuncSet.thy Thu Jul 08 08:42:36 2021 +0200 @@ -631,7 +631,7 @@ then show ?rhs apply (rule_tac x="f \<circ> inv_into (Collect P) g" in exI) unfolding o_def - by (metis (mono_tags, hide_lams) f_inv_into_f imageI inv_into_into mem_Collect_eq) + by (metis (mono_tags, opaque_lifting) f_inv_into_f imageI inv_into_into mem_Collect_eq) qed auto lemma function_factors_left: