diff -r b086f4e1722f -r 5de31ddf9c03 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Mon Jan 15 10:29:13 2001 +0100
+++ b/doc-src/IsarRef/pure.tex	Tue Jan 16 00:22:43 2001 +0100
@@ -442,6 +442,8 @@
 \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))
 \end{verbatim}
 }