--- a/src/Doc/Implementation/Local_Theory.thy Wed Jul 06 11:29:51 2016 +0200
+++ b/src/Doc/Implementation/Local_Theory.thy Wed Jul 06 14:09:13 2016 +0200
@@ -91,8 +91,8 @@
text %mlref \<open>
\begin{mldecls}
@{index_ML_type local_theory: Proof.context} \\
- @{index_ML Named_Target.init: "(local_theory -> local_theory) -> string ->
- theory -> local_theory"} \\[1ex]
+ @{index_ML Named_Target.init: "(local_theory -> local_theory) option ->
+ 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 ->