diff -r e5df9c8d9d4b -r bf085daea304 src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Mon Jun 08 15:09:57 2020 +0200
+++ b/src/Doc/System/Server.thy	Mon Jun 08 21:38:41 2020 +0200
@@ -515,9 +515,9 @@
 
   \<^item> \<^bold>\<open>type\<close> \<open>node = {node_name: string, theory_name: string}\<close> represents the
   internal node name of a theory. The \<open>node_name\<close> is derived from the
-  canonical theory file-name (e.g.\ \<^verbatim>\<open>"~~/src/HOL/ex/Seq.thy"\<close> after
+  canonical theory file-name (e.g.\ \<^verbatim>\<open>"~~/src/HOL/Examples/Seq.thy"\<close> after
   normalization within the file-system). The \<open>theory_name\<close> is the
-  session-qualified theory name (e.g.\ \<^verbatim>\<open>HOL-ex.Seq\<close>).
+  session-qualified theory name (e.g.\ \<^verbatim>\<open>HOL-Examples.Seq\<close>).
 
   \<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
   int, warned: int, failed: int, finished: int, canceled: bool, consolidated:
@@ -975,8 +975,8 @@
   The \<open>master_dir\<close> field specifies the master directory of imported theories:
   it acts like the ``current working directory'' for locating theory files.
   This is irrelevant for \<open>theories\<close> with an absolute path name (e.g.\
-  \<^verbatim>\<open>"~~/src/HOL/ex/Seq.thy"\<close>) or session-qualified theory name (e.g.\
-  \<^verbatim>\<open>"HOL-ex/Seq"\<close>).
+  \<^verbatim>\<open>"~~/src/HOL/Examples/Seq.thy"\<close>) or session-qualified theory name (e.g.\
+  \<^verbatim>\<open>"HOL-Examples.Seq"\<close>).
 
   \<^medskip>
   The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The
@@ -1026,7 +1026,7 @@
   Process some example theory from the Isabelle distribution, within the
   context of an already started session for Isabelle/HOL (see also
   \secref{sec:command-session-start}):
-  @{verbatim [display] \<open>use_theories {"session_id": ..., "theories": ["~~/src/HOL/ex/Seq"]}\<close>}
+  @{verbatim [display] \<open>use_theories {"session_id": ..., "theories": ["~~/src/HOL/Examples/Seq"]}\<close>}
 
   \<^medskip>
   Process some example theories in the context of their (single) parent