diff -r 3c576c7f9731 -r 1bd1d8492931 src/Doc/Implementation/Integration.thy
--- a/src/Doc/Implementation/Integration.thy	Mon Apr 04 15:53:56 2016 +0200
+++ b/src/Doc/Implementation/Integration.thy	Mon Apr 04 16:14:22 2016 +0200
@@ -152,7 +152,6 @@
 text %mlref \<open>
   \begin{mldecls}
   @{index_ML use_thy: "string -> unit"} \\
-  @{index_ML use_thys: "string list -> unit"} \\[0.5ex]
   @{index_ML Thy_Info.get_theory: "string -> theory"} \\
   @{index_ML Thy_Info.remove_thy: "string -> unit"} \\
   @{index_ML Thy_Info.register_thy: "theory -> unit"} \\
@@ -161,14 +160,6 @@
   \<^descr> @{ML use_thy}~\<open>A\<close> ensures that theory \<open>A\<close> is fully up-to-date wrt.\ the
   external file store; outdated ancestors are reloaded on demand.
 
-  \<^descr> @{ML use_thys} is similar to @{ML use_thy}, but handles several theories
-  simultaneously. Thus it acts like processing the import header of a theory,
-  without performing the merge of the result. By loading a whole sub-graph of
-  theories, the intrinsic parallelism can be exploited by the system to
-  speedup loading.
-
-  This variant is used by default in @{tool build} @{cite "isabelle-system"}.
-
   \<^descr> @{ML Thy_Info.get_theory}~\<open>A\<close> retrieves the theory value presently
   associated with name \<open>A\<close>. Note that the result might be outdated wrt.\ the
   file-system content.