src/Doc/Implementation/Logic.thy

   @{define_ML_type proof_body} \\
   @{define_ML Proofterm.proofs: "int Unsynchronized.ref"} \\
   @{define_ML Proofterm.reconstruct_proof:
   "theory -> term -> proof -> proof"} \\
   @{define_ML Proofterm.expand_proof: "theory ->
-  (Proofterm.thm_header -> Thm_Name.T option) -> proof -> proof"} \\
+  (Proofterm.thm_header -> Thm_Name.P option) -> proof -> proof"} \\
   @{define_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\
   @{define_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
   @{define_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\
   \end{mldecls}