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