# HG changeset patch
# User wenzelm
# Date 1236596268 -3600
# Node ID 910290f0469290c1a10ee7292b85cfad02a22335
# Parent  a59d792d0ccf8efeac9396b9c2e7ae8783edbfc8
adapted ThyOutput.antiquotation;

diff -r a59d792d0ccf -r 910290f04692 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Mon Mar 09 11:56:34 2009 +0100
+++ b/doc-src/antiquote_setup.ML	Mon Mar 09 11:57:48 2009 +0100
@@ -35,8 +35,8 @@
 
 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
 
-val _ = ThyOutput.antiquotation "verbatim" (fn _ => fn _ =>
-  Scan.lift Args.name >> (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
+val _ = ThyOutput.antiquotation "verbatim" (Scan.lift Args.name)
+  (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
 
 
 (* ML text *)