1.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Fri Mar 13 19:53:09 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Fri Mar 13 19:58:26 2009 +0100
     1.3 @@ -899,11 +899,10 @@
     1.4  %FIXME proper antiquotations
     1.5  {\footnotesize
     1.6  \begin{verbatim}
     1.7 - Method.no_args (Method.METHOD (fn facts => foobar_tac))
     1.8 - Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
     1.9 - Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
    1.10 - Method.thms_ctxt_args (fn thms => fn ctxt =>
    1.11 -    Method.METHOD (fn facts => foobar_tac))
    1.12 + Method.no_args (METHOD (fn facts => foobar_tac))
    1.13 + Method.thms_args (fn thms => METHOD (fn facts => foobar_tac))
    1.14 + Method.ctxt_args (fn ctxt => METHOD (fn facts => foobar_tac))
    1.15 + Method.thms_ctxt_args (fn thms => fn ctxt => METHOD (fn facts => foobar_tac))
    1.16  \end{verbatim}
    1.17  }
    1.18