# 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 *)