diff -r 3b80e7cf6629 -r d8d1f70024bd doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Thu Aug 17 18:58:49 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Thu Aug 17 21:06:04 2000 +0200
@@ -396,7 +396,7 @@
 \indexisarmeth{rule-tac}\indexisarmeth{erule-tac}
 \indexisarmeth{drule-tac}\indexisarmeth{frule-tac}
 \indexisarmeth{cut-tac}\indexisarmeth{thin-tac}
-\indexisarmeth{subgoal-tac}\indexisarmeth{rename_tac}
+\indexisarmeth{subgoal-tac}\indexisarmeth{rename-tac}
 \indexisarmeth{rotate-tac}\indexisarmeth{tactic}
 \begin{matharray}{rcl}
   rule_tac^* & : & \isarmeth \\