src/HOL/Computational_Algebra/Formal_Laurent_Series.thy

--- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Tue Oct 08 16:14:36 2024 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Tue Oct 08 16:15:31 2024 +0200
@@ -4601,11 +4601,11 @@
 
 subsection \<open>Notation\<close>
 
-no_notation fls_nth (infixl \<open>$$\<close> 75)
-
 bundle fps_syntax
 begin
 notation fls_nth (infixl \<open>$$\<close> 75)
 end
 
+unbundle no fps_syntax
+
 end
\ No newline at end of file