--- a/src/Doc/Implementation/Tactic.thy Thu Mar 19 17:25:57 2015 +0100
+++ b/src/Doc/Implementation/Tactic.thy Thu Mar 19 22:30:57 2015 +0100
@@ -394,10 +394,14 @@
text %mlref \<open>
\begin{mldecls}
- @{index_ML res_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
- @{index_ML eres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
- @{index_ML dres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
- @{index_ML forw_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
+ @{index_ML res_inst_tac: "Proof.context ->
+ ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\
+ @{index_ML eres_inst_tac: "Proof.context ->
+ ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\
+ @{index_ML dres_inst_tac: "Proof.context ->
+ ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\
+ @{index_ML forw_inst_tac: "Proof.context ->
+ ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\
@{index_ML subgoal_tac: "Proof.context -> string -> int -> tactic"} \\
@{index_ML thin_tac: "Proof.context -> string -> int -> tactic"} \\
@{index_ML rename_tac: "string list -> int -> tactic"} \\