diff -r 69880fdc8310 -r efb7fd4a6d1f src/Doc/Implementation/Prelim.thy
--- a/src/Doc/Implementation/Prelim.thy	Fri Jul 17 20:35:43 2020 +0200
+++ b/src/Doc/Implementation/Prelim.thy	Mon Jul 20 23:45:29 2020 +0200
@@ -269,23 +269,27 @@
   \begin{tabular}{ll}
   \<open>\<type> T\<close> & representing type \\
   \<open>\<val> empty: T\<close> & empty default value \\
-  \<open>\<val> extend: T \<rightarrow> T\<close> & re-initialize on import \\
-  \<open>\<val> merge: T \<times> T \<rightarrow> T\<close> & join on import \\
+  \<open>\<val> extend: T \<rightarrow> T\<close> & obsolete (identity function) \\
+  \<open>\<val> merge: T \<times> T \<rightarrow> T\<close> & merge data \\
   \end{tabular}
   \<^medskip>
 
   The \<open>empty\<close> value acts as initial default for \<^emph>\<open>any\<close> theory that does not
-  declare actual data content; \<open>extend\<close> acts like a unitary version of
-  \<open>merge\<close>.
+  declare actual data content; \<open>extend\<close> is obsolete: it needs to be the
+  identity function.
 
-  Implementing \<open>merge\<close> can be tricky. The general idea is that \<open>merge (data\<^sub>1,
-  data\<^sub>2)\<close> inserts those parts of \<open>data\<^sub>2\<close> into \<open>data\<^sub>1\<close> that are not yet
-  present, while keeping the general order of things. The \<^ML>\<open>Library.merge\<close>
-  function on plain lists may serve as canonical template.
+  The \<open>merge\<close> operation needs to join the data from two theories in a
+  conservative manner. The standard scheme for \<open>merge (data\<^sub>1, data\<^sub>2)\<close>
+  inserts those parts of \<open>data\<^sub>2\<close> into \<open>data\<^sub>1\<close> that are not yet present,
+  while keeping the general order of things. The \<^ML>\<open>Library.merge\<close>
+  function on plain lists may serve as canonical template. Particularly note
+  that shared parts of the data must not be duplicated by naive concatenation,
+  or a theory graph that resembles a chain of diamonds would cause an
+  exponential blowup!
 
-  Particularly note that shared parts of the data must not be duplicated by
-  naive concatenation, or a theory graph that is like a chain of diamonds
-  would cause an exponential blowup!
+  Sometimes, the data consists of a single item that cannot be ``merged'' in a
+  sensible manner. Then the standard scheme degenerates to the projection to
+  \<open>data\<^sub>1\<close>, ignoring \<open>data\<^sub>2\<close> outright.
 \<close>
 
 paragraph \<open>Proof context data\<close>