src/Doc/Implementation/Logic.thy

   @{index_ML Thm.add_def: "Proof.context -> bool -> bool ->
   binding * term -> theory -> (string * thm) * theory"} \\
   \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}
 
   \item @{ML Thm.peek_status}~@{text "thm"} informs about the current

   the returned theorem.
 
   \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>