diff -r a9694a4e39e5 -r bc9479cada96 doc-src/IsarImplementation/Thy/document/Isar.tex
--- a/doc-src/IsarImplementation/Thy/document/Isar.tex	Thu Jan 26 15:29:11 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Isar.tex	Thu Jan 26 21:16:11 2012 +0100
@@ -428,7 +428,6 @@
   \indexdef{}{ML}{METHOD}\verb|METHOD: (thm list -> tactic) -> Proof.method| \\
   \indexdef{}{ML}{SIMPLE\_METHOD}\verb|SIMPLE_METHOD: tactic -> Proof.method| \\
   \indexdef{}{ML}{SIMPLE\_METHOD'}\verb|SIMPLE_METHOD': (int -> tactic) -> Proof.method| \\
-  \indexdef{}{ML}{HEADGOAL}\verb|HEADGOAL: (int -> tactic) -> tactic| \\
   \indexdef{}{ML}{Method.insert\_tac}\verb|Method.insert_tac: thm list -> int -> tactic| \\
   \indexdef{}{ML}{Method.setup}\verb|Method.setup: binding -> (Proof.context -> Proof.method) context_parser ->|\isasep\isanewline%
 \verb|  string -> theory -> theory| \\
@@ -452,12 +451,8 @@
   applied.
 
   \item \verb|SIMPLE_METHOD'|~\isa{tactic} wraps a tactic that
-  addresses a specific subgoal as simple proof method.  Goal facts are
-  already inserted into the first subgoal before \isa{tactic} is
-  applied to the same.
-
-  \item \verb|HEADGOAL|~\isa{tactic} applies \isa{tactic} to
-  the first subgoal.  This is convenient to reproduce part the \verb|SIMPLE_METHOD'| wrapping within regular \verb|METHOD|, for example.
+  addresses a specific subgoal as simple proof method that operates on
+  subgoal 1.  Goal facts are inserted into the subgoal then the \isa{tactic} is applied.
 
   \item \verb|Method.insert_tac|~\isa{facts\ i} inserts \isa{facts} into subgoal \isa{i}.  This is convenient to reproduce
   part of the \verb|SIMPLE_METHOD| or \verb|SIMPLE_METHOD'| wrapping