diff -r e19d5b459a61 -r 4120fc59dd85 doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Fri Mar 13 19:53:09 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Fri Mar 13 19:58:26 2009 +0100
@@ -899,11 +899,10 @@
 %FIXME proper antiquotations
 {\footnotesize
 \begin{verbatim}
- Method.no_args (Method.METHOD (fn facts => foobar_tac))
- Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
- Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
- Method.thms_ctxt_args (fn thms => fn ctxt =>
-    Method.METHOD (fn facts => foobar_tac))
+ Method.no_args (METHOD (fn facts => foobar_tac))
+ Method.thms_args (fn thms => METHOD (fn facts => foobar_tac))
+ Method.ctxt_args (fn ctxt => METHOD (fn facts => foobar_tac))
+ Method.thms_ctxt_args (fn thms => fn ctxt => METHOD (fn facts => foobar_tac))
 \end{verbatim}
 }