--- a/src/Doc/Implementation/Logic.thy Tue Sep 22 20:29:20 2015 +0200
+++ b/src/Doc/Implementation/Logic.thy Tue Sep 22 22:38:22 2015 +0200
@@ -667,7 +667,7 @@
\end{mldecls}
\begin{mldecls}
@{index_ML Theory.add_deps: "Proof.context -> string ->
- Theory.dep -> Theory.dep list -> theory -> theory"} \\
+ Defs.entry -> Defs.entry list -> theory -> theory"} \\
\end{mldecls}
\begin{description}
@@ -766,7 +766,7 @@
\item @{ML Theory.add_deps}~@{text "ctxt name c\<^sub>\<tau> \<^vec>d\<^sub>\<sigma>"}
declares dependencies of a named specification for constant @{text
"c\<^sub>\<tau>"}, relative to existing specifications for constants @{text
- "\<^vec>d\<^sub>\<sigma>"}.
+ "\<^vec>d\<^sub>\<sigma>"}. This also works for type constructors.
\end{description}
\<close>