diff -r f614c619b1e1 -r a54ca4e90874 doc-src/IsarImplementation/Thy/proof.thy
--- 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}