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;

--- 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