
diff -r cf97438b0232 -r 233aba197bf2 doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Wed May 07 17:21:04 1997 +0200
+++ b/doc-src/Ref/thm.tex	Wed May 07 17:21:24 1997 +0200
@@ -557,7 +557,7 @@
 \subsection{Instantiation of unknowns}
 \index{instantiation}
 \begin{ttbox} 
-instantiate: (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
+instantiate: (indexname * ctyp){\thinspace}list * (cterm * cterm){\thinspace}list -> thm -> thm
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{instantiate} ($tyinsts$, $insts$) $thm$] 




