diff -r 2f831a45d571 -r 245b64afefe2 doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Fri Dec 05 17:31:01 1997 +0100
+++ b/doc-src/Ref/theories.tex	Fri Dec 05 18:44:56 1997 +0100
@@ -588,7 +588,7 @@
 incr_boundvars : int -> term -> term
 abstract_over  : term*term -> term
 variant_abs    : string * typ * term -> string * term
-aconv          : term*term -> bool\hfill{\bf infix}
+aconv          : term * term -> bool\hfill{\bf infix}
 \end{ttbox}
 These functions are all concerned with the de Bruijn representation of
 bound variables.