1.1 --- a/doc-src/isar.sty	Fri Mar 17 17:12:07 2000 +0100
     1.2 +++ b/doc-src/isar.sty	Fri Mar 17 22:49:13 2000 +0100
     1.3 @@ -86,7 +86,7 @@
     1.4  \newcommand{\CMT}[1]{\CMTNAME~\text{#1}}
     1.5  \newcommand{\ALSO}{\isarkeyword{also}}
     1.6  \newcommand{\FINALLY}{\isarkeyword{finally}}
     1.7 -\newcommand{\OBTAIN}[3]{\OBTAINNAME~#1\isarkeyword{where}~\I@optname{#2}~#3}
     1.8 +\newcommand{\OBTAIN}[3]{\OBTAINNAME~#1~\isarkeyword{where}\I@optname{#2}~#3}
     1.9  \newcommand{\BG}{\isarkeyword{\{\{}}
    1.10  \newcommand{\EN}{\isarkeyword{\}\}}}
    1.11  \newcommand{\NEXT}{\isarkeyword{next}}