diff -r 4dd3d5efcc7f -r a1e409db516b doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Sat Aug 09 12:28:13 2008 +0200
+++ b/doc-src/antiquote_setup.ML	Sat Aug 09 22:43:46 2008 +0200
@@ -30,7 +30,7 @@
   | clean_name "}" = "braceright"
   | clean_name s = s |> translate_string (fn "_" => "-" | c => c);
 
-val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
+val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src;
 
 fun tweak_line s =
   if ! O.display then s else Symbol.strip_blanks s;