# HG changeset patch
# User wenzelm
# Date 1226608864 -3600
# Node ID 8358fabeea9546bbf37b0709dcf4228517b98c57
# Parent  4ce896a30f8860ca2a103a85df9c1b127203e984
ignore ThyOutput.source flag;

diff -r 4ce896a30f88 -r 8358fabeea95 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Thu Nov 13 21:40:30 2008 +0100
+++ b/doc-src/antiquote_setup.ML	Thu Nov 13 21:41:04 2008 +0100
@@ -68,7 +68,7 @@
     val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
   in
     "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
-    ((if ! O.source then ThyOutput.str_of_source src else txt')
+    (txt'
     |> (if ! O.quotes then quote else I)
     |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
         else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))