--- 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}
}