adapted ThyOutput.antiquotation;
authorwenzelm
Mon, 09 Mar 2009 11:57:48 +0100
changeset 30382 910290f04692
parent 30381 a59d792d0ccf
child 30383 ee2c7592e59f
adapted ThyOutput.antiquotation;
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 *)