src/Doc/Implementation/Local_Theory.thy

 \<close>
 
 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: "(local_theory -> local_theory) -> 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 ->
     local_theory -> (string * thm list) * local_theory"} \\
   \end{mldecls}