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;