src/HOL/Computational_Algebra/Formal_Laurent_Series.thy

   unfolding open_dist subset_eq by simp
 
 
 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