diff -r 499a63c30d55 -r 96691631c1eb src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Sat Apr 09 12:36:25 2016 +0200
+++ b/src/Doc/Implementation/Logic.thy	Sat Apr 09 13:28:32 2016 +0200
@@ -1188,8 +1188,8 @@
   @{index_ML_type proof_body} \\
   @{index_ML proofs: "int Unsynchronized.ref"} \\
   @{index_ML Reconstruct.reconstruct_proof:
-  "theory -> term -> proof -> proof"} \\
-  @{index_ML Reconstruct.expand_proof: "theory ->
+  "Proof.context -> term -> proof -> proof"} \\
+  @{index_ML Reconstruct.expand_proof: "Proof.context ->
   (string * term option) list -> proof -> proof"} \\
   @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\
   @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
@@ -1221,7 +1221,7 @@
   records full proof terms. Officially named theorems that contribute to a
   result are recorded in any case.
 
-  \<^descr> @{ML Reconstruct.reconstruct_proof}~\<open>thy prop prf\<close> turns the implicit
+  \<^descr> @{ML Reconstruct.reconstruct_proof}~\<open>ctxt prop prf\<close> turns the implicit
   proof term \<open>prf\<close> into a full proof of the given proposition.
 
   Reconstruction may fail if \<open>prf\<close> is not a proof of \<open>prop\<close>, or if it does not
@@ -1229,7 +1229,7 @@
   for proofs that are constructed manually, but not for those produced
   automatically by the inference kernel.
 
-  \<^descr> @{ML Reconstruct.expand_proof}~\<open>thy [thm\<^sub>1, \<dots>, thm\<^sub>n] prf\<close> expands and
+  \<^descr> @{ML Reconstruct.expand_proof}~\<open>ctxt [thm\<^sub>1, \<dots>, thm\<^sub>n] prf\<close> expands and
   reconstructs the proofs of all specified theorems, with the given (full)
   proof. Theorems that are not unique specified via their name may be
   disambiguated by giving their proposition.