--- a/src/Doc/Implementation/Local_Theory.thy Fri Aug 04 08:12:37 2017 +0200
+++ b/src/Doc/Implementation/Local_Theory.thy Fri Aug 04 08:12:37 2017 +0200
@@ -91,8 +91,7 @@
text %mlref \<open>
\begin{mldecls}
@{index_ML_type local_theory: Proof.context} \\
- @{index_ML Named_Target.init: "(local_theory -> local_theory) option ->
- string -> theory -> local_theory"} \\[1ex]
+ @{index_ML Named_Target.init: "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 ->