src/HOL/Library/Lattice_Algebras.thy

   fixes a :: "'a\<Colon>{lattice_ab_group_add, linorder}"
   shows "sup a (- a) = (if a < 0 then - a else a)"
 proof -
   note add_le_cancel_right [of a a "- a", symmetric, simplified]
   moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
-  then show ?thesis by (auto simp: sup_max min_max.sup_absorb1 min_max.sup_absorb2)
+  then show ?thesis by (auto simp: sup_max max.absorb1 max.absorb2)
 qed
 
 lemma abs_if_lattice:
   fixes a :: "'a\<Colon>{lattice_ab_group_add_abs, linorder}"
   shows "\<bar>a\<bar> = (if a < 0 then - a else a)"