# HG changeset patch
# User wenzelm
# Date 1236078758 -3600
# Node ID 0abadde7b3fb0535c451ad54d64c0562c8786bc0
# Parent  e33ce8d765b433e1d07cf1db5acb373ddc6c7c41
ignore "source" option in antiquotations @{ML}, @{ML_type}, @{ML_struct} -- did not really make sense, without it users can enable source mode globally with less surprises;

diff -r e33ce8d765b4 -r 0abadde7b3fb src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Mar 02 20:31:27 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Mar 03 12:12:38 2009 +0100
@@ -519,9 +519,9 @@
 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
 
-fun output_ml ml src ctxt (txt, pos) =
+fun output_ml ml _ ctxt (txt, pos) =
  (ML_Context.eval_in (SOME ctxt) false pos (ml txt);
-  (if ! source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos)))
+  SymbolPos.content (SymbolPos.explode (txt, pos))
   |> (if ! quotes then quote else I)
   |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
   else