diff -r 8f3204e28783 -r c4677a6aae2c src/HOL/Library/Poly_Mapping.thy
--- a/src/HOL/Library/Poly_Mapping.thy	Tue May 02 14:19:34 2023 +0200
+++ b/src/HOL/Library/Poly_Mapping.thy	Tue May 02 19:49:17 2023 +0200
@@ -910,7 +910,7 @@
   is "\<lambda>f g. less_fun f g \<or> f = g"
   .
 
-instance proof (rule class.Orderings.linorder.of_class.intro)
+instance proof (rule linorder.intro_of_class)
   show "class.linorder (less_eq :: (_ \<Rightarrow>\<^sub>0 _) \<Rightarrow> _) less"
   proof (rule linorder_strictI, rule order_strictI)
     fix f g h :: "'a \<Rightarrow>\<^sub>0 'b"