Tuned section about parsing and printing proof terms.

--- a/doc-src/Ref/thm.tex	Fri Sep 28 17:19:46 2001 +0200
+++ b/doc-src/Ref/thm.tex	Fri Sep 28 18:55:37 2001 +0200
@@ -947,10 +947,10 @@
 or axiom. In contrast to term arguments, type arguments may
 be completely omitted.
 \begin{ttbox}
-  val read_proof : theory -> bool -> string -> Proofterm.proof
-  val pretty_proof : Sign.sg -> Proofterm.proof -> Pretty.T
-  val pretty_proof_of : bool -> thm -> Pretty.T
-  val print_proof_of : bool -> thm -> unit
+ProofSyntax.read_proof : theory -> bool -> string -> Proofterm.proof
+ProofSyntax.pretty_proof : Sign.sg -> Proofterm.proof -> Pretty.T
+ProofSyntax.pretty_proof_of : bool -> thm -> Pretty.T
+ProofSyntax.print_proof_of : bool -> thm -> unit
 \end{ttbox}
 \begin{figure}
 \begin{center}