diff -r 50ca726466c6 -r 0a604b2fc2b1 doc-src/Ref/goals.tex
--- a/doc-src/Ref/goals.tex	Sun Oct 31 15:26:37 1999 +0100
+++ b/doc-src/Ref/goals.tex	Sun Oct 31 20:11:23 1999 +0100
@@ -186,14 +186,14 @@
   stores $thm$ in the theorem database associated with its theory and
   returns that theorem.
   
-\item[\ttindexbold{bind_thms} and \ttindexbold{store_thms}] are similar to
+\item[\ttindexbold{bind_thms} \textrm{and} \ttindexbold{store_thms}] are similar to
   \texttt{bind_thm} and \texttt{store_thm}, but store lists of theorems.
 
 \end{ttdescription}
 
-The name argument of \texttt{qed}, \texttt{bind_thm} etc.\ may be empty
-(\texttt{""}) as well; in that case the result is \emph{not} stored, but
-proper checks and presentation of the result still apply.
+The name argument of \texttt{qed}, \texttt{bind_thm} etc.\ may be the empty
+string as well; in that case the result is \emph{not} stored, but proper
+checks and presentation of the result still apply.
 
 
 \subsection{Extracting axioms and stored theorems}