diff -r 4918c6e52a02 -r 15865e0c5598 src/Doc/Implementation/Logic.thy
--- 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>