doc-src/isar.sty

--- a/doc-src/isar.sty	Mon Aug 23 15:24:00 1999 +0200
+++ b/doc-src/isar.sty	Mon Aug 23 15:27:27 1999 +0200
@@ -57,7 +57,7 @@
 \newcommand{\DEFS}{\isarkeyword{defs}}
 \newcommand{\TEXT}{\isarkeyword{text}}
 \newcommand{\TXT}{\isarkeyword{txt}}
-\newcommand{\NOTE}[2]{\NOTENAME\ifthenelse{\equal{}{#1}}{}{~#1=}#2}
+\newcommand{\NOTE}[2]{\NOTENAME~\ifthenelse{\equal{}{#1}}{}{#1=}#2}
 \newcommand{\FROM}[1]{\FROMNAME~#1}
 \newcommand{\WITH}[1]{\WITHNAME~#1}
 \newcommand{\FIX}[1]{\FIXNAME~#1}