--- a/src/HOL/List.thy Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/List.thy Thu Jul 08 08:42:36 2021 +0200
@@ -990,7 +990,7 @@
\<and> (xs' = [] \<or> ys' = [] \<or> hd xs' \<noteq> hd ys')"
by (induct xs ys rule: list_induct2')
(blast, blast, blast,
- metis (no_types, hide_lams) append_Cons append_Nil list.sel(1))
+ metis (no_types, opaque_lifting) append_Cons append_Nil list.sel(1))
text \<open>Trivial rules for solving \<open>@\<close>-equations automatically.\<close>
@@ -1146,7 +1146,7 @@
by (iprover dest: map_injective injD intro: inj_onI)
lemma inj_mapD: "inj (map f) \<Longrightarrow> inj f"
- by (metis (no_types, hide_lams) injI list.inject list.simps(9) the_inv_f_f)
+ by (metis (no_types, opaque_lifting) injI list.inject list.simps(9) the_inv_f_f)
lemma inj_map[iff]: "inj (map f) = inj f"
by (blast dest: inj_mapD intro: inj_mapI)