--- a/src/HOL/Library/Lexord.thy Wed Mar 09 12:43:48 2022 +0000
+++ b/src/HOL/Library/Lexord.thy Wed Mar 09 16:21:58 2022 +0000
@@ -189,10 +189,7 @@
global_interpretation dvd: lex_preordering \<open>(dvd) :: 'a::comm_monoid_mult \<Rightarrow> 'a \<Rightarrow> bool\<close> dvd_strict
defines lex_dvd = dvd.lex_less_eq
and lex_dvd_strict = dvd.lex_less
- apply (rule lex_preordering.intro)
- apply standard
- apply (auto simp add: dvd_strict_def)
- done
+ by unfold_locales (auto simp add: dvd_strict_def)
global_interpretation lex_dvd: preordering lex_dvd lex_dvd_strict
by (fact dvd.preordering)