diff -r 9d62b37bbfca -r 242527763a16 doc-src/isar.sty
--- 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}}