# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1646842918 0
# Node ID f70b1a2c27832648c9b4b0064f6cc8a0429bd82e
# Parent  a2b8394ce1f158b8b444138822149565f9504f19
A tiny further cleanup

diff -r a2b8394ce1f1 -r f70b1a2c2783 src/HOL/Library/Lexord.thy
--- 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)