diff -r bad7156a7814 -r dff7dfd8dce3 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Tue Oct 08 16:14:36 2024 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Tue Oct 08 16:15:31 2024 +0200
@@ -6191,11 +6191,11 @@
 qed
 
 (* TODO: Figure out better notation for this thing *)
-no_notation fps_nth (infixl \<open>$\<close> 75)
-
 bundle fps_syntax
 begin
 notation fps_nth (infixl \<open>$\<close> 75)
 end
 
+unbundle no fps_syntax
+
 end