diff -r 849efff7de15 -r ad5fc948e053 src/HOL/Computational_Algebra/Formal_Laurent_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Wed Oct 02 22:08:52 2024 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Wed Oct 02 23:47:07 2024 +0200
@@ -25,7 +25,7 @@
 
 setup_lifting type_definition_fls
 
-unbundle fps_notation
+unbundle fps_syntax
 notation fls_nth (infixl \<open>$$\<close> 75)
 
 lemmas fls_eqI = iffD1[OF fls_nth_inject, OF iffD2, OF fun_eq_iff, OF allI]
@@ -4603,7 +4603,7 @@
 
 no_notation fls_nth (infixl \<open>$$\<close> 75)
 
-bundle fls_notation
+bundle fps_syntax
 begin
 notation fls_nth (infixl \<open>$$\<close> 75)
 end