diff -r 66bff50bc5f1 -r fd21b4a93043 src/HOL/Nominal/Examples/Class1.thy --- a/src/HOL/Nominal/Examples/Class1.thy Fri Jun 18 15:03:12 2021 +0200 +++ b/src/HOL/Nominal/Examples/Class1.thy Thu Jul 08 08:42:36 2021 +0200 @@ -1707,7 +1707,7 @@ case (AndR c1 M c2 M' c3) then show ?case apply(auto simp add: fresh_prod calc_atm fresh_atm abs_fresh fresh_left) - apply (metis (erased, hide_lams)) + apply (metis (erased, opaque_lifting)) by metis next case AndL1