src/Doc/System/Server.thy

   argument: & \<open>use_theories_arguments\<close> \\
   regular result: & \<^verbatim>\<open>OK\<close> \<open>use_theories_results\<close> \\
   \end{tabular}
 
   \begin{tabular}{ll}
-  \<^bold>\<open>type\<close> \<open>theory_name = string | {name: string, pos: position}\<close> \\
-  \end{tabular}
-
-  \begin{tabular}{ll}
   \<^bold>\<open>type\<close> \<open>use_theories_arguments =\<close> \\
   \quad\<open>{session_id: uuid,\<close> \\
-  \quad~~\<open>theories: [theory_name],\<close> \\
+  \quad~~\<open>theories: [string],\<close> \\
   \quad~~\<open>master_dir?: string,\<close> \\
   \quad~~\<open>pretty_margin?: double\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
   \quad~~\<open>unicode_symbols?: bool}\<close> \\[2ex]
   \end{tabular}
 

   The \<open>session_id\<close> is the identifier provided by the server, when the session
   was created (possibly on a different client connection).
 
   \<^medskip>
   The \<open>theories\<close> field specifies theory names as in theory \<^theory_text>\<open>imports\<close> or in
-  ROOT \<^bold>\<open>theories\<close>. An explicit source position for these theory name
-  specifications may be given, which is occasionally useful for precise error
-  locations.
+  ROOT \<^bold>\<open>theories\<close>.
 
   \<^medskip> 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 may be omitted if all entries of \<open>theories\<close> use a
   session-qualified theory name (e.g.\ \<^verbatim>\<open>"HOL-Library.AList"\<close>) or absolute