diff -r f4c614ece7ed -r 7219a771ab63 doc-src/IsarImplementation/Thy/Proof.thy
--- a/doc-src/IsarImplementation/Thy/Proof.thy	Fri Oct 15 19:19:41 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Proof.thy	Fri Oct 15 19:54:34 2010 +0100
@@ -382,11 +382,10 @@
   conclusion: the proof demonstrates that the context may be augmented
   by parameters and assumptions, without affecting any conclusions
   that do not mention these parameters.  See also
-  \cite{isabelle-isar-ref} for the user-level @{text "\<OBTAIN>"} and
-  @{text "\<GUESS>"} elements.  Final results, which may not refer to
+  \cite{isabelle-isar-ref} for the user-level @{command obtain} and
+  @{command guess} elements.  Final results, which may not refer to
   the parameters in the conclusion, need to exported explicitly into
-  the original context.
-*}
+  the original context.  *}
 
 text %mlref {*
   \begin{mldecls}
@@ -444,4 +443,25 @@
   \end{description}
 *}
 
+text %mlex {* The following example demonstrates forward-elimination
+  in a local context, using @{ML Obtain.result}.
+*}
+
+example_proof
+  assume ex: "\<exists>x. B x"
+
+  ML_prf %"ML" {*
+    val ctxt0 = @{context};
+    val (([(_, x)], [B]), ctxt1) = ctxt0
+      |> Obtain.result (fn _ => etac @{thm exE} 1) [@{thm ex}];
+  *}
+  ML_prf %"ML" {*
+    singleton (ProofContext.export ctxt1 ctxt0) @{thm refl};
+  *}
+  ML_prf %"ML" {*
+    ProofContext.export ctxt1 ctxt0 [Thm.reflexive x]
+      handle ERROR msg => (warning msg; []);
+  *}
+qed
+
 end