adapted ThyOutput.antiquotation;
authorwenzelm
Mon Mar 09 11:57:48 2009 +0100 (2009-03-09)
changeset 30382910290f04692
parent 30381 a59d792d0ccf
child 30383 ee2c7592e59f
adapted ThyOutput.antiquotation;
doc-src/antiquote_setup.ML
     1.1 --- a/doc-src/antiquote_setup.ML	Mon Mar 09 11:56:34 2009 +0100
     1.2 +++ b/doc-src/antiquote_setup.ML	Mon Mar 09 11:57:48 2009 +0100
     1.3 @@ -35,8 +35,8 @@
     1.4  
     1.5  val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
     1.6  
     1.7 -val _ = ThyOutput.antiquotation "verbatim" (fn _ => fn _ =>
     1.8 -  Scan.lift Args.name >> (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
     1.9 +val _ = ThyOutput.antiquotation "verbatim" (Scan.lift Args.name)
    1.10 +  (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
    1.11  
    1.12  
    1.13  (* ML text *)