--- a/doc-src/IsarImplementation/Thy/proof.thy Thu Sep 14 21:42:21 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy Thu Sep 14 22:48:37 2006 +0200
@@ -295,7 +295,7 @@
@{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
@{index_ML Obtain.result: "(Proof.context -> tactic) ->
- thm list -> Proof.context -> (cterm list * thm list) * Proof.context"}
+ thm list -> Proof.context -> (cterm list * thm list) * Proof.context"} \\
\end{mldecls}
\begin{description}