--- a/src/Doc/Implementation/Logic.thy Tue Jul 30 13:22:29 2019 +0200
+++ b/src/Doc/Implementation/Logic.thy Tue Jul 30 14:35:29 2019 +0200
@@ -1179,9 +1179,9 @@
@{index_ML_type proof} \\
@{index_ML_type proof_body} \\
@{index_ML Proofterm.proofs: "int Unsynchronized.ref"} \\
- @{index_ML Reconstruct.reconstruct_proof:
+ @{index_ML Proofterm.reconstruct_proof:
"Proof.context -> term -> proof -> proof"} \\
- @{index_ML Reconstruct.expand_proof: "Proof.context ->
+ @{index_ML Proofterm.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"} \\
@@ -1213,7 +1213,7 @@
additionally records full proof terms. Officially named theorems that
contribute to a result are recorded in any case.
- \<^descr> \<^ML>\<open>Reconstruct.reconstruct_proof\<close>~\<open>ctxt prop prf\<close> turns the implicit
+ \<^descr> \<^ML>\<open>Proofterm.reconstruct_proof\<close>~\<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
@@ -1221,7 +1221,7 @@
for proofs that are constructed manually, but not for those produced
automatically by the inference kernel.
- \<^descr> \<^ML>\<open>Reconstruct.expand_proof\<close>~\<open>ctxt [thm\<^sub>1, \<dots>, thm\<^sub>n] prf\<close> expands and
+ \<^descr> \<^ML>\<open>Proofterm.expand_proof\<close>~\<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.