recovered "\<phi>\<^isub>i" from 0b02aaf7c7c5;

--- a/src/Doc/IsarImplementation/Tactic.thy	Wed Jul 31 22:15:17 2013 +0200
+++ b/src/Doc/IsarImplementation/Tactic.thy	Wed Jul 31 23:41:32 2013 +0200
@@ -509,7 +509,7 @@
   regarded as an atomic formula, to solve premise @{text "i"} of
   @{text "thm\<^sub>2"}.  Let @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} be @{text
   "\<psi>"} and @{text "\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>"}.  The unique @{text "s"} that
-  unifies @{text "\<psi>"} and @{text "\<phi>"} yields the theorem @{text "(\<phi>\<^sub>1 \<Longrightarrow>
+  unifies @{text "\<psi>"} and @{text "\<phi>\<^isub>i"} yields the theorem @{text "(\<phi>\<^sub>1 \<Longrightarrow>
   \<dots> \<phi>\<^sub>i\<^sub>-\<^sub>1 \<Longrightarrow> \<phi>\<^sub>i\<^sub>+\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>)s"}.  Multiple results are considered as
   error (exception @{ML THM}).