diff -r a9b20bc32fa6 -r ead56ad40e15 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Mon Sep 20 23:15:02 2021 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Tue Sep 21 00:20:47 2021 +0200
@@ -89,7 +89,7 @@
 
 \subsubsection*{Syntax}
 
-Available by loading theory \<open>Lattice_Syntax\<close> in directory \<open>Library\<close>.
+Available via \<^theory_text>\<open>unbundle lattice_syntax\<close>.
 
 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
 @{text[source]"x \<sqsubseteq> y"} & \<^term>\<open>x \<le> y\<close>\\