tuned

--- a/src/Doc/ProgProve/Isar.thy	Mon Feb 10 23:24:44 2014 +0100
+++ b/src/Doc/ProgProve/Isar.thy	Tue Feb 11 09:29:46 2014 +0100
@@ -372,7 +372,7 @@
 then obtain x where p: "P(x)" by blast
 (*<*)oops(*>*)
 text{*
-After the \isacom{obtain} step, @{text x} (we could have chosen any name)
+After the \indexed{\isacom{obtain}}{obtain} step, @{text x} (we could have chosen any name)
 is a fixed local
 variable, and @{text p} is the name of the fact
 \noquotes{@{prop[source] "P(x)"}}.