proper signature;
authorwenzelm
Wed, 06 Jul 2016 14:09:13 +0200
changeset 63403 a962f349c8c9
parent 63402 f199837304d7
child 63404 a95e7432d86c
proper signature;
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 ->