# HG changeset patch
# User wenzelm
# Date 1521920874 -3600
# Node ID cb2b1a75ff59d3b7ace3c578e9715ee5768ada36
# Parent  b45f0c0ea14f51ebcf3160b535164d844db24dd6
tuned;

diff -r b45f0c0ea14f -r cb2b1a75ff59 src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Sat Mar 24 20:45:30 2018 +0100
+++ b/src/Doc/System/Server.thy	Sat Mar 24 20:47:54 2018 +0100
@@ -890,17 +890,11 @@
   \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}
-
-  \begin{tabular}{ll}
-  \<^bold>\<open>type\<close> \<open>node_result =\<close> \\
-  \quad\<open>{status: node_status,\<close> \\
-  \quad~~\<open>messages: [message]}\<close> \\[2ex]
 
   \<^bold>\<open>type\<close> \<open>use_theories_results =\<close> \\
   \quad\<open>{ok: bool,\<close> \\
   \quad~~\<open>errors: [message],\<close> \\
-  \quad~~\<open>nodes: [node \<oplus> node_result]}\<close> \\[2ex]
+  \quad~~\<open>nodes: [node \<oplus> {status: node_status, messages: [message]}]}\<close> \\
   \end{tabular}
 
   \<^medskip>