diff -r b3b95a228d37 -r 280436a346ca doc-src/TutorialI/isa-index
--- a/doc-src/TutorialI/isa-index	Wed Jul 11 13:55:15 2001 +0200
+++ b/doc-src/TutorialI/isa-index	Wed Jul 11 13:55:43 2001 +0200
@@ -16,8 +16,8 @@
 # change *IDENT  to  IDENT@{\tt IDENT}  
 #    where IDENT is any string not containing | ! or @
 # FOUR backslashes: to escape the shell AND sed
-sed -e "s~\*\(\".\".\".\".\)~\1@{\\\\isa{\1}}~g
-s~\*\(\".\".\".\)~\1@{\\\\isa{\1}}~g
-s~\*\(\".\".\)~\1@{\\\\isa{\1}}~g
-s~\*\(\".\)~\1@{\\\\isa{\1}}~g
-s~\*\([^ |!@{}][^ |!@{}]*\)~\1@{\\\\isa{\1}}~g" $1.idx | makeindex -c -q -o $1.ind
+sed -e "s~\*\(\".\".\".\".\)~\1@\\\\isa {\1}~g
+s~\*\(\".\".\".\)~\1@\\\\isa {\1}~g
+s~\*\(\".\".\)~\1@\\\\isa {\1}~g
+s~\*\(\".\)~\1@\\\\isa {\1}~g
+s~\*\([^ |!@{}][^ |!@{}]*\)~\1@\\\\isa {\1}~g" $1.idx | makeindex -c -q -o $1.ind