diff -r 7cb68b5b103d -r 589645894305 src/Doc/Implementation/Local_Theory.thy
--- a/src/Doc/Implementation/Local_Theory.thy	Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Doc/Implementation/Local_Theory.thy	Sun Nov 01 16:54:49 2020 +0100
@@ -91,7 +91,7 @@
 text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type local_theory: Proof.context} \\
-  @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex]
+  @{index_ML Named_Target.init: "string list -> string -> theory -> local_theory"} \\[1ex]
   @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
     local_theory -> (term * (string * thm)) * local_theory"} \\
   @{index_ML Local_Theory.note: "Attrib.binding * thm list ->
@@ -104,7 +104,7 @@
   context data. Subtyping means that any value \<open>lthy:\<close>~\<^ML_type>\<open>local_theory\<close>
   can be also used with operations on expecting a regular \<open>ctxt:\<close>~\<^ML_type>\<open>Proof.context\<close>.
 
-  \<^descr> \<^ML>\<open>Named_Target.init\<close>~\<open>before_exit name thy\<close> initializes a local theory
+  \<^descr> \<^ML>\<open>Named_Target.init\<close>~\<open>includes name thy\<close> initializes a local theory
   derived from the given background theory. An empty name refers to a \<^emph>\<open>global
   theory\<close> context, and a non-empty name refers to a @{command locale} or
   @{command class} context (a fully-qualified internal name is expected here).