doc-src/Ref/goals.tex
changeset 4374 245b64afefe2
parent 4317 7264fa2ff2ec
child 5205 602354039306
--- a/doc-src/Ref/goals.tex	Fri Dec 05 17:31:01 1997 +0100
+++ b/doc-src/Ref/goals.tex	Fri Dec 05 18:44:56 1997 +0100
@@ -157,7 +157,7 @@
   \ttindex{assume_ax} has been used.
   
 \item[\ttindexbold{bind_thm} ($name$, $thm$);]\index{theorems!storing}
-  stores {\tt standard($thm$)} (see \S\ref{MiscellaneousForwardRules})
+  stores {\tt standard $thm$} (see \S\ref{MiscellaneousForwardRules})
   in the theorem database associated with its theory and in the {\ML}
   variable $name$.  The theorem can be retrieved from the database
   using {\tt get_thm} (see \S\ref{BasicOperationsOnTheories}).