# HG changeset patch
# User wenzelm
# Date 1467806953 -7200
# Node ID a962f349c8c9fba030d30bd13ca6ea24b2ad494d
# Parent  f199837304d7aa9aa27242f672257c10e61e9541
proper signature;

diff -r f199837304d7 -r a962f349c8c9 src/Doc/Implementation/Local_Theory.thy
--- 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 ->