src/Doc/Implementation/Logic.thy

   @{index_ML Logic.mk_implies: "term * term -> term"} \\
   \end{mldecls}
   \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"} \\
   @{index_ML Drule.mk_implies: "cterm * cterm -> cterm"} \\
   \end{mldecls}

   same inference kernel that is mainly responsible for @{ML_type thm}.
   Thus syntactic operations on @{ML_type ctyp} and @{ML_type cterm}
   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.
 
   \item @{ML Thm.apply}, @{ML Thm.lambda}, @{ML Thm.all}, @{ML
   Drule.mk_implies} etc.\ compose certified terms (or propositions)