diff -r e6f03fae14d5 -r ddb2da7cb2e4 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Thu Sep 24 13:33:42 2015 +0200
+++ b/src/Doc/Implementation/Logic.thy	Thu Sep 24 23:33:29 2015 +0200
@@ -662,11 +662,11 @@
   binding * term -> theory -> (string * thm) * theory"} \\
   @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->
   (string * ('a -> thm)) * theory"} \\
-  @{index_ML Thm.add_def: "Proof.context -> bool -> bool ->
+  @{index_ML Thm.add_def: "Defs.context -> bool -> bool ->
   binding * term -> theory -> (string * thm) * theory"} \\
   \end{mldecls}
   \begin{mldecls}
-  @{index_ML Theory.add_deps: "Proof.context -> string ->
+  @{index_ML Theory.add_deps: "Defs.context -> string ->
   Defs.entry -> Defs.entry list -> theory -> theory"} \\
   \end{mldecls}