diff -r 92d7d8e4f1bf -r 291934bac95e src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/Doc/Implementation/Logic.thy	Fri Mar 06 15:58:56 2015 +0100
@@ -639,8 +639,8 @@
   \begin{mldecls}
   @{index_ML_type ctyp} \\
   @{index_ML_type cterm} \\
-  @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
-  @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
+  @{index_ML Thm.ctyp_of: "Proof.context -> typ -> ctyp"} \\
+  @{index_ML Thm.cterm_of: "Proof.context -> term -> cterm"} \\
   @{index_ML Thm.apply: "cterm -> cterm -> cterm"} \\
   @{index_ML Thm.lambda: "cterm -> cterm -> cterm"} \\
   @{index_ML Thm.all: "cterm -> cterm -> cterm"} \\
@@ -699,10 +699,11 @@
   are located in the @{ML_structure Thm} module, even though theorems are
   not yet involved at that stage.
 
-  \item @{ML Thm.ctyp_of}~@{text "thy \<tau>"} and @{ML
-  Thm.cterm_of}~@{text "thy t"} explicitly checks types and terms,
+  \item @{ML Thm.ctyp_of}~@{text "ctxt \<tau>"} and @{ML
+  Thm.cterm_of}~@{text "ctxt t"} explicitly check types and terms,
   respectively.  This also involves some basic normalizations, such
-  expansion of type and term abbreviations from the theory context.
+  expansion of type and term abbreviations from the underlying
+  theory context.
   Full re-certification is relatively slow and should be avoided in
   tight reasoning loops.