diff -r 0c5cd369a643 -r 50b60f501b05 src/Doc/Implementation/Tactic.thy
--- a/src/Doc/Implementation/Tactic.thy	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/Doc/Implementation/Tactic.thy	Tue Feb 10 14:48:26 2015 +0100
@@ -277,11 +277,11 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML resolve_tac: "thm list -> int -> tactic"} \\
-  @{index_ML eresolve_tac: "thm list -> int -> tactic"} \\
-  @{index_ML dresolve_tac: "thm list -> int -> tactic"} \\
-  @{index_ML forward_tac: "thm list -> int -> tactic"} \\
-  @{index_ML biresolve_tac: "(bool * thm) list -> int -> tactic"} \\[1ex]
+  @{index_ML resolve_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{index_ML eresolve_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{index_ML dresolve_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{index_ML forward_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{index_ML biresolve_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\[1ex]
   @{index_ML assume_tac: "Proof.context -> int -> tactic"} \\
   @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex]
   @{index_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\
@@ -292,20 +292,20 @@
 
   \begin{description}
 
-  \item @{ML resolve_tac}~@{text "thms i"} refines the goal state
+  \item @{ML resolve_tac}~@{text "ctxt thms i"} refines the goal state
   using the given theorems, which should normally be introduction
   rules.  The tactic resolves a rule's conclusion with subgoal @{text
   i}, replacing it by the corresponding versions of the rule's
   premises.
 
-  \item @{ML eresolve_tac}~@{text "thms i"} performs elim-resolution
+  \item @{ML eresolve_tac}~@{text "ctxt thms i"} performs elim-resolution
   with the given theorems, which are normally be elimination rules.
 
-  Note that @{ML "eresolve_tac [asm_rl]"} is equivalent to @{ML
-  assume_tac}, which facilitates mixing of assumption steps with
+  Note that @{ML_text "eresolve_tac ctxt [asm_rl]"} is equivalent to @{ML_text
+  "assume_tac ctxt"}, which facilitates mixing of assumption steps with
   genuine eliminations.
 
-  \item @{ML dresolve_tac}~@{text "thms i"} performs
+  \item @{ML dresolve_tac}~@{text "ctxt thms i"} performs
   destruct-resolution with the given theorems, which should normally
   be destruction rules.  This replaces an assumption by the result of
   applying one of the rules.
@@ -314,7 +314,7 @@
   selected assumption is not deleted.  It applies a rule to an
   assumption, adding the result as a new assumption.
 
-  \item @{ML biresolve_tac}~@{text "brls i"} refines the proof state
+  \item @{ML biresolve_tac}~@{text "ctxt brls i"} refines the proof state
   by resolution or elim-resolution on each rule, as indicated by its
   flag.  It affects subgoal @{text "i"} of the proof state.