diff -r 689e2bd78c19 -r 5a54c796b808 doc-src/Ref/syntax.tex
--- a/doc-src/Ref/syntax.tex	Fri Jul 29 13:28:39 1994 +0200
+++ b/doc-src/Ref/syntax.tex	Fri Jul 29 13:30:48 1994 +0200
@@ -423,7 +423,7 @@
 \end{itemize}
 
 Macro rules may refer to any syntax from the parent theories.  They may
-also refer to anything defined before the the {\tt .thy} file's {\tt
+also refer to anything defined before the {\tt .thy} file's {\tt
   translations} section --- including any mixfix declarations.
 
 Upon declaration, both sides of the macro rule undergo parsing and parse