--- a/src/HOL/Examples/Coherent.thy	Tue Oct 08 17:26:31 2024 +0200
+++ b/src/HOL/Examples/Coherent.thy	Tue Oct 08 22:56:27 2024 +0200
@@ -11,7 +11,8 @@
 
 subsection \<open>Equivalence of two versions of Pappus' Axiom\<close>
 
-no_notation comp  (infixl \<open>o\<close> 55) and relcomp  (infixr \<open>O\<close> 75)
+no_notation comp  (infixl \<open>o\<close> 55)
+unbundle no relcomp_syntax
 
 lemma p1p2:
   assumes "col a b c l \<and> col d e f m"