doc-src/antiquote_setup.ML
changeset 27809 a1e409db516b
parent 27353 71c4dd53d4cb
child 28217 21f0c2de0a38
     1.1 --- a/doc-src/antiquote_setup.ML	Sat Aug 09 12:28:13 2008 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Sat Aug 09 22:43:46 2008 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4    | clean_name "}" = "braceright"
     1.5    | clean_name s = s |> translate_string (fn "_" => "-" | c => c);
     1.6  
     1.7 -val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
     1.8 +val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src;
     1.9  
    1.10  fun tweak_line s =
    1.11    if ! O.display then s else Symbol.strip_blanks s;